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

29 files changed, 0 insertions, 58 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 35db5e6ed1..0068921895 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index a97b85ed94..afda6d9315 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.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/proofs/clenvtac.ml b/proofs/clenvtac.ml
index f977768bd6..a8162cc5a4 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 02bf86641b..760a79d4ce 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.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/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6dfbbdc121..cd05cdcd25 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Util
 open Names
 open Term
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index ff986f3e66..ca3bd1e802 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Term
 open Environ
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a9202318df..4e5905d831 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesscer General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Term
 
 (* This module implements the abstract interface to goals *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 49e3c9b1ae..c7f6957662 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: goal.mli aspiwack $ *)
-
 (* This module implements the abstract interface to goals *)
 
 type goal
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 7c092bb66e..93de5be692 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/proofs/logic.mli b/proofs/logic.mli
index eec3de7303..39f69ad127 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.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/proofs/pfedit.ml b/proofs/pfedit.ml
index 6da73c2f67..153354c920 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 47b741f5d5..194dd14648 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Util
 open Pp
 open Names
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0c298cc630..35f7b4f023 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* Module defining the last essential tiles of interactive proofs.
    The features of the Proof module are undoing and focusing.
    A proof is a mutable object, it contains a proofview, and some information
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 2b1c3f5c20..5e1120f9c0 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proof.mli aspiwack $ *)
-
 (* Module defining the last essential tiles of interactive proofs.
    The features of the Proof module are undoing and focusing.
    A proof is a mutable object, it contains a proofview, and some information
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 420ff84325..87a8d8d1e2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (***********************************************************************)
 (*                                                                     *)
 (*      This module defines the global proof environment               *)
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 84a61c755a..40908dfc44 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (***********************************************************************)
 (*                                                                     *)
 (*      This module defines the global proof environment               *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 2fffa39527..55a73c608b 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ *)
-
 (*i*)
 open Environ
 open Evd
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 7d88753021..8def611129 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Environ
 open Evd
 open Names
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a08941df03..427a8d6136 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* The proofview datastructure is a pure datastructure underlying the notion
    of proof (namely, a proof is a proofview which can evolve and has safety
    mechanisms attached).
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index cd5520d4e5..dc205f538a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proofview.mli aspiwack $ *)
-
 (* The proofview datastructure is a pure datastructure underlying the notion
    of proof (namely, a proof is a proofview which can evolve and has safety
    mechanisms attached).
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index b0a01caa7b..b300977317 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 199130b5f3..581ee1dc9b 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Term
 open Closure
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ffb18f2655..1abd762538 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Term
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9585600446..be4dbd9a5f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Term
 open Sign
 open Evd
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b56e5184e0..4cec846fd3 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Topconstr
 open Libnames
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6dbdf17cb8..8104295199 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index cf704d101c..9e0ca2a3d6 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.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/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index f6b2ce4525..a3fa59e8a6 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Constrextern
 open Pp
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index f275403152..ac3bf493a9 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Environ
 open Pattern
 open Evd