Remove the svn-specific $Id$ annotations

 - Many of them were broken, some of them after Pierre B's rework
   of mli for ocamldoc, but not only (many bad annotation, many files
   with no svn property about Id, etc)
 - Useless for those of us that work with git-svn (and a fortiori
   in a forthcoming git-only setting)
 - Even in svn, they seem to be of little interest

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

26 files changed, 0 insertions, 53 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 99c627a95..fec00c65a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (*i*)
 open Pp
 open Util
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ac9ed5714..ac3a38833 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Util
 open Names
 open Term
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2b16023f0..ecaba603d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Flags
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4ba2bc587..bf28e0850 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Term
 open Sign
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 1ca82e35c..6cfe1421f 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Util
 open Pp
 open Names
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 5148461a9..a80e749d3 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Libnames
 open Nametab
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 702c509dc..9dfa808c7 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 
 (* Dump of globalization (to be used by coqdoc) *)
 
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 7235fe172..7efa6f1e0 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -6,9 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(** {% $ %}Id: dumpglob.mli 11252 2008-07-24 11:16:48Z notin {% $ %} *)
-
-
 val open_glob_file : string -> unit
 val close_glob_file : unit -> unit
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 241c92582..e5950cd8d 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 50abd351e..984f479fb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Util
 open Names
 open Term
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d5894b208..89ec5f1f1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*i*)
 open Names
 open Decl_kinds
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 7362d7de5..ac610fe78 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Decl_kinds
 open Term
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 049745ca9..094b723e0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/interp/modintern.mli b/interp/modintern.mli
index e025447b5..5dacfd070 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Declarations
 open Environ
 open Entries
diff --git a/interp/notation.ml b/interp/notation.ml
index 794169a37..bfa86b50f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (*i*)
 open Util
 open Pp
diff --git a/interp/notation.mli b/interp/notation.mli
index 91f262b48..224fb1d45 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Util
 open Pp
 open Bigint
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index a4142d694..16d0537b9 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ *)
-
 (*i*)
 open Pp
 open Util
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 984696cda..19ca913e8 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Pp
 open Names
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 9d8412825..700fcd1e3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (* Reserved names *)
 
 open Util
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 4cc2eff5a..e53ad8365 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Util
 open Names
 open Rawterm
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index faad3c50a..424e7cc1e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -11,8 +11,6 @@
 
 (* This file provides high-level name globalization functions *)
 
-(* $Id:$ *)
-
 (* *)
 open Pp
 open Util
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index b505e7db7..0cd261a82 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(** {% $ %}Id:{% $ %} *)
-
 open Util
 open Names
 open Libnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 245ed0f50..334135eaf 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Util
 open Pp
 open Names
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 6b57b497a..019067608 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Util
 open Names
 open Topconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c0b624110..5fade008c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (*i*)
 open Pp
 open Util
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 02e6d1eeb..2b9506747 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Pp
 open Util
 open Names