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

20 files changed, 24 insertions, 24 deletions

diff --git a/toplevel/class.mli b/toplevel/class.mli
index 57d395c207..8c8a647848 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8c34a3eb16..ec43a2efb9 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 86b2c9b64e..a0b3d5911b 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Initialization. *)
 
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 3a97b3b921..53af17474a 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input 
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 935432f8eb..7cd5aab39c 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* This module implements the discharge mechanism. It provides a function to
    close the last opened section. That function calls [Lib.close_section] and
diff --git a/toplevel/errors.mli b/toplevel/errors.mli
index 4f6a1a0743..2fe4e91880 100644
--- a/toplevel/errors.mli
+++ b/toplevel/errors.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 5680af6f57..7823c73478 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index fabe326348..b679227581 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli
index 866cfc3df8..cfaa1a3180 100644
--- a/toplevel/line_oriented_parser.mli
+++ b/toplevel/line_oriented_parser.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 val line_oriented_channel_to_option: string -> in_channel -> int -> char option
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index e3d9e593d7..fc4ef2968a 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Extend
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 37a71d212c..467395c1ec 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* If there is a toplevel under Coq, it is described by the following 
    record. *)
diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli
index f618c517f4..0046f4a53b 100644
--- a/toplevel/protectedtoplevel.mli
+++ b/toplevel/protectedtoplevel.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 842754b9ad..c3fbb70f23 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli
index 40323c0ec4..b6d773cd02 100644
--- a/toplevel/searchisos.mli
+++ b/toplevel/searchisos.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 val search_in_lib : bool ref
 val type_search : Term.constr -> unit
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index b2509d0119..ac807a99a4 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 3a4ed2b9b4..c89239b6b7 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*s Prints the version number on the standard output and exits (with 0). *)
 
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 0c65b86931..5e9c71d19c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Parsing of vernacular. *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 47675e0df9..fd58ae3ed5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -732,7 +732,7 @@ let _ =
 	   fun () ->
              begin
                start_proof_com (Some s) stre com;
-               if (not(is_silent())) then show_open_subgoals()
+               if not (is_silent()) then show_open_subgoals()
              end
        | _ -> bad_vernac_args "StartProof")
 
@@ -811,7 +811,7 @@ let _ =
 	     definition_body_red red_option id (local,stre) c typ_opt;
              if coe then begin
 	       Class.try_add_new_coercion id stre;
-               if (not (is_silent())) then
+               if not (is_silent()) then
 		 message ((string_of_id id) ^ " is now a coercion")
 	     end;
 	     if idcoe then 
@@ -1230,7 +1230,7 @@ let _ =
 	   in
 	   fun () -> 
 	     Class.try_add_new_class id stre;
-             if (not (is_silent())) then
+             if not (is_silent()) then
                message ((string_of_id id) ^ " is now a class")
        | _ -> bad_vernac_args "CLASS")
 
@@ -1248,7 +1248,7 @@ let _ =
 	   let isid = identity = "IDENTITY" in
 	   fun () -> 
 	     Class.try_add_new_coercion_with_target id stre ids idt isid;
-             if (not (is_silent())) then
+             if not (is_silent()) then
 	       message ((string_of_id id) ^ " is now a coercion")
        | _ -> bad_vernac_args "COERCION")
 
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 9fbe7574cb..68b78ee6ab 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 4fe1b54c90..0c136820a7 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Names