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

22 files changed, 0 insertions, 44 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 0a75f01375..0317416f30 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: library.ml 9679 2007-02-24 15:22:07Z herbelin $ *)
-
 open Pp
 open Util
 open Names
diff --git a/checker/checker.ml b/checker/checker.ml
index e15c37e670..9489dc94b7 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml 10153 2007-09-28 18:00:45Z glondu $ *)
-
 open Pp
 open Util
 open System
diff --git a/checker/closure.ml b/checker/closure.ml
index c710df816e..054057d1ff 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: closure.ml 9983 2007-07-12 17:15:22Z barras $ *)
-
 open Util
 open Pp
 open Term
diff --git a/checker/closure.mli b/checker/closure.mli
index 260d159b3d..ada7ded1e3 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: closure.mli 9902 2007-06-21 17:01:21Z herbelin $ i*)
-
 (*i*)
 open Pp
 open Names
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index de57c50a74..0b4c6fde39 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *)
-
 open Util
 open Names
 open Univ
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index b920315ab5..12511df336 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: indtypes.mli 9831 2007-05-17 18:55:42Z herbelin $ i*)
-
 (*i*)
 open Names
 open Univ
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 4faf99a907..54bf1bbe62 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 10172 2007-10-04 13:02:03Z herbelin $ *)
-
 open Util
 open Names
 open Univ
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 8e6d4ffb99..bd758772a9 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*)
-
 (*i*)
 open Names
 open Term
diff --git a/checker/modops.ml b/checker/modops.ml
index ce2f07ab66..e6428d5ab4 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 9872 2007-05-30 16:01:18Z soubiran $ i*)
-
 (*i*)
 open Util
 open Pp
diff --git a/checker/modops.mli b/checker/modops.mli
index 4476013c67..fedcf32cbd 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
 (*i*)
 open Util
 open Names
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 612e7562fa..776edb2436 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
-
 open Util
 open Names
 open Term
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 81c93ee53f..02b856edcf 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: reduction.mli 7639 2005-12-02 10:01:15Z gregoire $ i*)
-
 (*i*)
 open Term
 open Environ
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 98534e08ca..e37ff370c0 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 10275 2007-10-30 11:01:24Z barras $ *)
-
 open Pp
 open Util
 open Names
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 12fdbfce80..ded3fe47f0 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: safe_typing.mli 9821 2007-05-11 17:00:58Z aspiwack $ i*)
-
 (*i*)
 open Names
 open Term
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index ec1c908a60..9df49630c5 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
-
 (*i*)
 open Util
 open Names
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index 10842252e0..1b0ca5c167 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
 (*i*)
 open Univ
 open Term
diff --git a/checker/term.ml b/checker/term.ml
index 35ae1121e4..8d65bbe176 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
-
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
 open Util
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index 7c01410559..bddda852d2 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: type_errors.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
-
 open Names
 open Term
 open Environ
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 0482f2f2a8..70971faa4c 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: type_errors.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
-
 (*i*)
 open Names
 open Term
diff --git a/checker/typeops.ml b/checker/typeops.ml
index e5cf6a6d6d..1007c8971c 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
-
 open Util
 open Names
 open Univ
diff --git a/checker/typeops.mli b/checker/typeops.mli
index de160a79b8..d554af0262 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeops.mli 9427 2006-12-11 18:46:35Z bgregoir $ i*)
-
 (*i*)
 open Names
 open Term
diff --git a/checker/validate.ml b/checker/validate.ml
index ab17aa7f82..d3d2ecb603 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* This module defines validation functions to ensure an imported
    value (using input_value) has the correct structure. *)