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

7 files changed, 0 insertions, 14 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 36da9463b..598b21d83 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 Require Export List.
 Require Export BinPos.
 
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 0d1d09c73..47fc11825 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 
 Require Export List.
 Require Export Bintree.
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 4cbe84368..6309a7425 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$*)
-
 (*i camlp4deps: "parsing/grammar.cma"  i*)
 
 TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 562e2e3bd..029e7eafd 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 open Term
 open Util
 open Goptions
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index e52f6bbdc..44a5f49c6 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 type form=
     Atom of int
   | Arrow of form * form
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 06313e8fe..3ae25da65 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
-
 module Search = Explore.Make(Proof_search)
 
 open Util
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index a6d68a226..79872f2cd 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 (* raises Not_found if no proof is found *)
 
 type atom_env=