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 73b51cfe7..18b3642e2 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 a68e72d26..6d33bd8ea 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 37721c9b9..33bac0e1c 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 dcb4601e5..243fe4db3 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 e7c2e23f7..e7b5f31fc 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 6bcd24763..7920a0302 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 579f42df5..84202d539 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 1b5dbc711..0a865bfcf 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 00df1a98d..effc7af46 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 df962773d..630a59e9d 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 0366c4ba7..8691d0181 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 9195b747e..7e8127fb3 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 8e04a368e..70d14fb27 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 5759cf0c2..3d980e65f 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 4a1c1778f..78cf59740 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 9cc34634a..6a44812da 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 b0fa395c6..51c73ef14 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 866f499b5..36ba0cd7d 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 512ecca74..b8cdea3b6 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