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 0a75f0137..0317416f3 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 e15c37e67..9489dc94b 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 c710df816..054057d1f 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 260d159b3..ada7ded1e 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 de57c50a7..0b4c6fde3 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 b920315ab..12511df33 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 4faf99a90..54bf1bbe6 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 8e6d4ffb9..bd758772a 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 ce2f07ab6..e6428d5ab 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 4476013c6..fedcf32cb 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 612e7562f..776edb243 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 81c93ee53..02b856edc 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 98534e08c..e37ff370c 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 12fdbfce8..ded3fe47f 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 ec1c908a6..9df49630c 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 10842252e..1b0ca5c16 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 35ae1121e..8d65bbe17 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 7c0141055..bddda852d 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 0482f2f2a..70971faa4 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 e5cf6a6d6..1007c8971 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 de160a79b..d554af026 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 ab17aa7f8..d3d2ecb60 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. *)