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 d2bb1a06f..32a199e60 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 37fe3d441..f7c3fd777 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 a0dea0292..2b05fcb65 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 a9556891a..bda1fc65f 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 bcb9a411c..13027fd34 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 ebb046a05..a4ace7637 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 e0e7aae2f..18d2c6081 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 46ed2134d..29604a95f 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 b5fdf5a1b..b74a23271 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 96d83b972..f45685eaf 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 465a2a377..c35b4d759 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 49af8b40e..ebef403a1 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 cac200f58..7baa5cd8c 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 7fbb16ba1..2351947e0 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 e3f29fe59..28c696010 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 ef1c4ec3e..d58878838 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 d5e4ca17d..a93be7bc6 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 51dbd7ecd..195d4b7c4 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 bdf3bbe76..8c649aecf 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 8a4fb392e..1a5a92fc3 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 b5c147393..d5694ba89 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 906c32c57..c8e6c9769 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 0cf4dbb80..ffce59547 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 adf8275ee..dd37822a1 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 3421ded92..ffa1bd747 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 8a68c9f20..a1c1da177 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 259fe8814..f2f13fe11 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 4fed5d27c..da2b49557 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 dae0281bd..120d42abf 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 b6112c34f..b20383969 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 40ad0da9b..3fa8596f9 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 46ca8161c..3130c1ca9 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 a7780206b..b038e4f0e 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 395a7c206..5c22bfd89 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 7d6e1c4c9..67b396dda 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 3f866d5da..5d80d847e 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 cb6cb961f..484954bcc 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 c9a4598e5..ef369a857 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 1af2d3398..fd34d70f9 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 6e3957ac0..86bd7cbee 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 771d28fba..7c731e2b9 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 8e5124c41..ff3abd1d2 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 208a76aef..d74bb0ebb 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 045f70c61..1ff67bffe 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 c357451a2..e67e11227 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 e6201aad9..21a9ee258 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 2d7c07402..8a413e137 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 60baa017c..2bb225c66 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 7b6d3ea76..fe5dc572d 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 973cc0e5b..ed3a928ab 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