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

16 files changed, 16 insertions, 16 deletions

diff --git a/lib/bij.mli b/lib/bij.mli
index 65bae1eec2..7e6d23e828 100644
--- a/lib/bij.mli
+++ b/lib/bij.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Bijections. *)
 
diff --git a/lib/bstack.mli b/lib/bstack.mli
index d1f9ae387e..fc646f1a4f 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Bounded stacks. If the depth is [None], then there is no depth limit. *)
 
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 2f2bb7b802..2c0587ee67 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Dynamics. Use with extreme care. Not for kids. *)
 
diff --git a/lib/edit.mli b/lib/edit.mli
index 5926456f0a..c86022e443 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* The type of editors.
  * An editor is a finite map, ['a -> 'b], which knows how to apply
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 908bad1bcf..a73bdba519 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Maps using the generic comparison function of ocaml. Same interface as
    the module [Map] from the ocaml standard library. *)
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index c3a55e8c1c..23c77851bc 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Maps from ['a] to lists of ['b]. *)
 
diff --git a/lib/gset.mli b/lib/gset.mli
index 645a29cad4..125fbe4422 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Sets using the generic comparison function of ocaml. Same interface as
    the module [Set] from the ocaml standard library. *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 9665e1a86b..07dd8bc2b0 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Generic hash-consing. *)
 
diff --git a/lib/options.mli b/lib/options.mli
index 25c194106b..d36c6a4678 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Global options of the system. *)
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 8906616ac4..96ef3d3ded 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp_control
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 6c92849a78..b6d6132e01 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Parameters of pretty-printing. *)
 
diff --git a/lib/profile.mli b/lib/profile.mli
index 893bf07b9e..6ba6a4489b 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Profiling. *)
 
diff --git a/lib/stamps.mli b/lib/stamps.mli
index 1eb624d57a..40a83feb69 100644
--- a/lib/stamps.mli
+++ b/lib/stamps.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Time stamps. *)
 
diff --git a/lib/system.mli b/lib/system.mli
index 71dff73c3b..a91562cea9 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*s Files and load paths. Load path entries remember the original root
     given by the user. For efficiency, we keep the full path (field
diff --git a/lib/tlm.mli b/lib/tlm.mli
index 44a2adc8bf..f046397504 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (* Tries. This module implements a data structure [('a,'b) t] mapping lists
    of values of type ['a] to sets (as lists) of values of type ['b]. *)
diff --git a/lib/util.mli b/lib/util.mli
index 1cb05ad6f1..fce150e803 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (*i*)
 open Pp