From af93e4cf8b1a839d21499b3b9737bb8904edcae8 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 29 Apr 2010 13:50:31 +0000
Subject: 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
---
 plugins/rtauto/Bintree.v        | 2 --
 plugins/rtauto/Rtauto.v         | 2 --
 plugins/rtauto/g_rtauto.ml4     | 2 --
 plugins/rtauto/proof_search.ml  | 2 --
 plugins/rtauto/proof_search.mli | 2 --
 plugins/rtauto/refl_tauto.ml    | 2 --
 plugins/rtauto/refl_tauto.mli   | 2 --
 7 files changed, 14 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 36da9463ba..598b21d834 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 0d1d09c736..47fc118259 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 4cbe843685..6309a74256 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 562e2e3bdb..029e7eafd1 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 e52f6bbdc5..44a5f49c68 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 06313e8fe7..3ae25da653 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 a6d68a2265..79872f2cdc 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=
-- 
cgit v1.2.3