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=