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

19 files changed, 0 insertions, 38 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 73b51cfe7d..18b3642e28 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Pp
 open Util
 open Names
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index a68e72d261..6d33bd8ea0 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Libnames
 open Miniml
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 37721c9b96..33bac0e1c3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Term
 open Declarations
 open Names
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index dcb4601e58..243fe4db34 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*s This module declares the extraction commands. *)
 
 open Names
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e7c2e23f7d..e7b5f31fce 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*i*)
 open Util
 open Names
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 6bcd24763f..7920a0302b 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*s Extraction from Coq terms to Miniml. *)
 
 open Names
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 579f42df5b..84202d5398 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*s Production of Haskell syntax. *)
 
 open Pp
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 1b5dbc7111..0a865bfcf2 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -6,7 +6,5 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 val haskell_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 00df1a98d3..effc7af468 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index df962773d0..630a59e9d8 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*i*)
 open Pp
 open Util
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 0366c4ba78..8691d01815 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.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/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9195b747e9..7e8127fb3e 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Declarations
 open Environ
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 8e04a368ed..70d14fb274 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Declarations
 open Environ
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 5759cf0c2a..3d980e65f0 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*s Production of Ocaml syntax. *)
 
 open Pp
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 4a1c1778f2..78cf597409 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -6,7 +6,5 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 val ocaml_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 9cc34634a9..6a44812da3 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*s Production of Scheme syntax. *)
 
 open Pp
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index b0fa395c63..51c73ef14f 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -6,6 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 val scheme_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 866f499b59..36ba0cd7d8 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Term
 open Declarations
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 512ecca743..b8cdea3b6a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Libnames
 open Miniml