From 31b1436a88b15929c694175e511e38eab79f2a89 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Sep 2014 09:37:10 -0700
Subject: [PATCH] doc(doc/server): update server documentation

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 doc/server.org | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/doc/server.org b/doc/server.org
index b4f4a4d80..8ab5d8ee1 100644
--- a/doc/server.org
+++ b/doc/server.org
@@ -137,6 +137,16 @@ The following two information entries provide information for Lean keywords/symb
 -- ACK
 #+END_SRC
 
+Information about introduced coercions is of the form
+
+#+BEGIN_SRC
+-- COERCION|[line-number]|[column-number]
+[coercion-application]
+--
+[result-type]
+-- ACK
+#+END_SRC
+
 Here is an example of output produced by Lean
 
 #+BEGIN_SRC
@@ -284,4 +294,3 @@ where each entry is of the form
 
 The available =kinds= are: =Bool=, =Int=, =Unsigned Int=, =Double=,
 =String=, and =S-Expressions=.
-