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

50 files changed, 0 insertions, 100 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d2bb1a06fc..32a199e607 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 37fe3d4418..f7c3fd7775 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.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/tactics/autorewrite.ml b/tactics/autorewrite.ml
index a0dea0292e..2b05fcb65f 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Equality
 open Hipattern
 open Names
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index a9556891a6..bda1fc65f3 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Term
 open Tacexpr
 open Tacmach
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index bcb9a411c0..13027fd348 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Term
 open Names
 open Termdn
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index ebb046a05f..a4ace7637b 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Term
 open Pattern
 open Names
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e0e7aae2fe..18d2c60814 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,8 +9,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 46ed2134d0..29604a95f2 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Util
 open Term
 open Proof_type
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index b5fdf5a1bc..b74a23271c 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Term
 open Proof_type
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 96d83b9724..f45685eafc 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* Chet's comments about this tactic :
 
  Programmable destruction of hypotheses and conclusions.
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index 465a2a377e..c35b4d759d 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Tacmach
 open Tacexpr
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 49af8b40ea..ebef403a17 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/elim.ml b/tactics/elim.ml
index cac200f58d..7baa5cd8c4 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 7fbb16ba1a..2351947e06 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Term
 open Proof_type
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e3f29fe596..28c6960101 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* Created by Hugo Herbelin from contents related to inductive schemes
    initially developed by Christine Paulin (induction schemes), Vincent
    Siles (decidable equality and boolean equality) and Matthieu Sozeau
diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli
index ef1c4ec3e2..d58878838e 100644
--- a/tactics/elimschemes.mli
+++ b/tactics/elimschemes.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(** {% $ %}Id: elimschemes.mli 12584 2009-12-13 21:04:34Z herbelin {% $ %} *)
-
 open Ind_tables
 
 (** Induction/recursion schemes *)
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index d5e4ca17d7..a93be7bc69 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -14,8 +14,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
-
 open Util
 open Names
 open Namegen
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 51dbd7ecdd..195d4b7c44 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* File created by Hugo Herbelin, Nov 2009 *)
 
 (* This file builds schemes related to equality inductive types,
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index bdf3bbe76c..8c649aecf4 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 (** This file builds schemes relative to equality inductive types *)
 
 open Names
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8a4fb392ea..1a5a92fc3f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/equality.mli b/tactics/equality.mli
index b5c147393d..d5694ba899 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (*i*)
 open Util
 open Names
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 906c32c57a..c8e6c9769c 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Term
 open Util
 open Evar_refiner
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 0cf4dbb809..ffce595477 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Tacmach
 open Names
 open Tacexpr
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index adf8275ee8..dd37822a1f 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
-
 open Pp
 open Pcoq
 open Genarg
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 3421ded92a..ffa1bd747c 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Tacexpr
 open Term
 open Names
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 8a68c9f20d..a1c1da177e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id$ *)
-
 open Pp
 open Pcoq
 open Genarg
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 259fe8814f..f2f13fe11b 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Proof_type
 
 val h_discrHyp : Names.identifier -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 4fed5d27cf..da2b49557f 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Term
 open Proof_type
 open Tacmach
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index dae0281bdb..120d42abf6 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -7,8 +7,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Names
 open Util
 open Term
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index b6112c34fb..b203839697 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 40ad0da9ba..3fa8596f90 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.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/tactics/inv.ml b/tactics/inv.ml
index 46ca8161c8..3130c1ca9b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/inv.mli b/tactics/inv.mli
index a7780206ba..b038e4f0e3 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.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/tactics/leminv.ml b/tactics/leminv.ml
index 395a7c206e..5c22bfd894 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 7d6e1c4c90..67b396dda2 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Util
 open Names
 open Term
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 3f866d5da2..5d80d847eb 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Term
 open Pattern
 open Libnames
diff --git a/tactics/refine.ml b/tactics/refine.ml
index cb6cb961f4..484954bcc7 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 (* JCF -- 6 janvier 1998  EXPERIMENTAL *)
 
 (*
diff --git a/tactics/refine.mli b/tactics/refine.mli
index c9a4598e59..ef369a8572 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Tacmach
 
 val refine : Evd.open_constr -> tactic
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1af2d33988..fd34d70f97 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -9,8 +9,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: rewrite.ml4 11981 2009-03-16 08:18:53Z herbelin $ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6e3957ac05..86bd7cbee8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Constrintern
 open Closure
 open RedFlags
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 771d28fbac..7c731e2b9c 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 8e5124c417..ff3abd1d2d 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 12623 2010-01-04 17:50:38Z letouzey $ *)
-
 open Libobject
 open Proof_type
 open Pp
diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli
index 208a76aefb..d74bb0ebb6 100644
--- a/tactics/tactic_option.mli
+++ b/tactics/tactic_option.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 12623 2010-01-04 17:50:38Z letouzey $ *)
-
 open Proof_type
 open Tacexpr
 open Vernacexpr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 045f70c61b..1ff67bffe5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index c357451a21..e67e11227a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e6201aad9d..21a9ee258e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Pp
 open Util
 open Names
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2d7c074029..8a413e1370 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.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/tactics/tauto.ml4 b/tactics/tauto.ml4
index 60baa017cf..2bb225c667 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id$ i*)
-
 open Term
 open Hipattern
 open Names
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 7b6d3ea767..fe5dc572dc 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Util
 open Names
 open Nameops
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 973cc0e5b6..ed3a928abb 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -6,8 +6,6 @@
            *       GNU Lesser General Public License Version 2.1        
   ***********************************************************************)
 
-(*i $Id$ i*)
-
 open Term
 open Pattern
 open Libnames