syntaxe AST Inversion + commentaires ocamlweb autour de $

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 19 insertions, 17 deletions

diff --git a/parsing/ast.mli b/parsing/ast.mli
index f40bc78b97..f77ef81239 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 6bf724bf84..1541abe64b 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 3a02092cd4..38803b5ae6 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Abstract syntax trees. *)
 
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index c581d9db07..47e477fc5c 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Coqast
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index a7da42b9c1..fe8542a51d 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 8fe219d459..086d1b2ebc 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index db5c0d07f5..7ebd657703 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -1,4 +1,6 @@
 
+(*i $Id$ i*)
+
 (*i*)
 open Pp
 open Names
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
index 61f305ad9c..f9b7b51d1f 100644
--- a/parsing/g_natsyntax.mli
+++ b/parsing/g_natsyntax.mli
@@ -1,4 +1,4 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Nice syntax for naturals. *)
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
index 310d09a12c..f04d6a151d 100644
--- a/parsing/g_zsyntax.mli
+++ b/parsing/g_zsyntax.mli
@@ -1,4 +1,4 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Nice syntax for integers. *)
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 2c7351bf10..8ecfbd0699 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 type error =
   | Illegal_character
diff --git a/parsing/pattern.mli b/parsing/pattern.mli
index b50f67ed82..5c5c28ba1b 100644
--- a/parsing/pattern.mli
+++ b/parsing/pattern.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7cf26bdd27..26ff046048 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* The lexer and parser of Coq. *)
 
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index b8bb0b1a10..0a1ed41f33 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/printer.mli b/parsing/printer.mli
index cbc70a2f48..fe456f047a 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/search.ml b/parsing/search.ml
index fca710e283..8369ba98c2 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -76,7 +76,7 @@ let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
 let search_by_head ref =
   crible (fun pname ass_name constr -> 
             let pc = prterm_env ass_name constr in
-            mSG[< pname; 'sTR":"; pc; 'fNL >]) ref
+            mSG [< hOV 2 [< pname; 'sTR":"; 'sPC; pc >]; 'fNL >]) ref
 
 (* Fine Search. By Yves Bertot. *)
 
@@ -96,7 +96,7 @@ let xor a b = (a or b) & (not (a & b))
 
 let plain_display s a c =
   let pc = Printer.prterm_env a c in
-  mSG [< s; 'sTR":"; pc; 'fNL>]
+  mSG [< hOV 2 [< s; 'sTR":"; 'sPC; pc >]; 'fNL>]
 
 let filter_by_module module_list accept _ _ c =
   try
diff --git a/parsing/search.mli b/parsing/search.mli
index 42e277a5d1..c0c003ad8a 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Pp
 open Term
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 68ef2f1d0f..4b689ead0b 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names