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 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= -- cgit v1.2.3