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 99c627a956..fec00c65ad 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 ac9ed5714b..ac3a388332 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 2b16023f0d..ecaba603d2 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 4ba2bc5871..bf28e0850a 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 1ca82e35c8..6cfe1421f7 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 5148461a97..a80e749d30 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 702c509dc7..9dfa808c73 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 7235fe1729..7efa6f1e01 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 241c92582a..e5950cd8d6 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 50abd351e7..984f479fb7 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 d5894b208c..89ec5f1f11 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 7362d7de56..ac610fe78d 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 049745ca9f..094b723e08 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 e025447b55..5dacfd0700 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 794169a377..bfa86b50f2 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 91f262b488..224fb1d45b 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 a4142d6949..16d0537b98 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 984696cdab..19ca913e88 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 9d8412825f..700fcd1e3a 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 4cc2eff5ad..e53ad8365a 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 faad3c50a4..424e7cc1ef 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 b505e7db7a..0cd261a82e 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 245ed0f508..334135eaf4 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 6b57b497ad..0190676084 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 c0b624110a..5fade008cf 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 02e6d1eeb5..2b95067473 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