diff options
| author | letouzey | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /toplevel | |
| parent | 0f61b02f84b41e1f019cd78824de28f18ff854aa (diff) | |
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
Diffstat (limited to 'toplevel')
44 files changed, 0 insertions, 88 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index d8c7326a9e..65eb45cb2a 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index b45e45c80d..fe13f28ee1 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - (*i*) open Pp open Printer diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 130b0b591a..4fe2dffa8c 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Indtypes diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index 8f26f44951..4ef5401d8a 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util diff --git a/toplevel/class.ml b/toplevel/class.ml index 0166b52135..ec623f7674 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Names diff --git a/toplevel/class.mli b/toplevel/class.mli index 4ee894cc97..51fb8b26e5 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Classops diff --git a/toplevel/classes.ml b/toplevel/classes.ml index b7860c8b09..40d44432eb 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Names open Decl_kinds diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 279622843f..cae779b08f 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Decl_kinds open Term diff --git a/toplevel/command.ml b/toplevel/command.ml index 51c7e50a47..fcc6c8acea 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Flags diff --git a/toplevel/command.mli b/toplevel/command.mli index 904a1a034e..446cdc1b33 100644 --- a/toplevel/command.mli +++ b/toplevel/command.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/toplevel/coqinit.ml b/toplevel/coqinit.ml index d9fcdb247e..a6cd938ae0 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open System open Toplevel diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index 9258594586..f209fd7384 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Initialization. *) val set_debug : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a88ee3ba6a..885f9ce9a9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open System diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 0c43cc757c..e4f1537a20 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** The Coq main module. The following function [start] will parse the command line, print the banner, initialize the load path, load the input state, load the files given on the command line, load the ressource file, diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 4c21e49154..700328c8c5 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Names open Util open Sign diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index b3636d7176..03f831c238 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Sign open Cooking open Declarations diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 0fb9a33b2b..6c8847ff95 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Flags diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 23c10767dc..464c8f89c4 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Names open Indtypes diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 447aeca48a..845a5697a0 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index b8f2986f3f..a5d15a28ab 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.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/toplevel/indschemes.mli b/toplevel/indschemes.mli index aab60a590d..291b66776f 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.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/toplevel/lemmas.ml b/toplevel/lemmas.ml index f80fbf201d..fb789798f3 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index 44502b4e42..55d7dcf2ee 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.fix_expr ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Decl_kinds diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 06b751c5f0..65aac9769a 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Flags open Util diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 63272b7d3e..f558fc4d18 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Libnames diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index ee43703050..509ecd89d1 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -11,8 +11,6 @@ * camlp4deps will not work for this file unless Makefile system enhanced. *) -(* $Id$ *) - open Util open Pp open Flags diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index a03ad6242e..9da3575816 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** If there is a toplevel under Coq, it is described by the following record. *) type toplevel = { diff --git a/toplevel/record.ml b/toplevel/record.ml index c1c1a96713..d95c3657e4 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/toplevel/record.mli b/toplevel/record.mli index d432bff6de..2090cf1e51 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Sign diff --git a/toplevel/search.ml b/toplevel/search.ml index 075c80c9a2..353caa2061 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/toplevel/search.mli b/toplevel/search.mli index a9d62c6efa..28096eb5ec 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Names open Term diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ee821a48d5..4535522734 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Flags diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index f51c088f04..8980ef92b6 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Pcoq diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 257660481f..d12cbb7627 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - let version () = Printf.printf "The Coq Proof Assistant, version %s (%s)\n" Coq_config.version Coq_config.date; diff --git a/toplevel/usage.mli b/toplevel/usage.mli index 1dfd4897b2..23e807c162 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Prints the version number on the standard output and exits (with 0). } *) val version : unit -> 'a diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 0bdb68f495..8386dd2b32 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Parsing of vernacular. *) open Pp diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 8ae319791b..01852f1305 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Parsing of vernacular. *) (** Read a vernac command on the specified input (parse only). diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 36f1e96e94..1ec553a9a0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* Concrete syntax of the mathematical vernacular MV V2.6 *) open Pp diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index fa9f2b7c2a..b70eb61fbc 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Vernacinterp diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index e216f25203..cbd6fb8dec 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Names open Tacexpr diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 0924e519bd..040a153a62 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 4c59eadba8..0a58b17b5f 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Tacexpr (** Interpretation of extended vernac phrases. *) diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 9d4b5ec0cf..6919a9730b 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Flags open Pp open Util diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index 4c14c836ae..72245021d3 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Coq interface to the Whelp query engine developed at the University of Bologna *) |