diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /library | |
| 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 'library')
34 files changed, 0 insertions, 68 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 5fd27f467..be2e79c70 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Libnames diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index abc201eb1..2c04d0fdd 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: decl_kinds.mli 12337 2009-09-17 15:58:14Z glondu {% $ %} *) - open Util open Libnames diff --git a/library/declare.ml b/library/declare.ml index a83a7b4b0..68b9ca9fb 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** This module is about the low-level declaration of logical objects *) open Pp diff --git a/library/declare.mli b/library/declare.mli index 1b4564d9c..db9e1aa6d 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Libnames open Term diff --git a/library/declaremods.ml b/library/declaremods.ml index bca52c556..42abebe86 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/library/declaremods.mli b/library/declaremods.mli index 17fd44024..4cbdf4ce4 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Entries diff --git a/library/decls.ml b/library/decls.ml index ac2203ccf..7243eb0f6 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** This module registers tables for some non-logical informations associated declarations *) diff --git a/library/decls.mli b/library/decls.mli index 091ec7d99..34a96cd8b 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Sign open Libnames diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 85de6ab8f..0154f4334 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Libnames open Names diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index bc9541cf4..b264c1228 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Libnames open Term open Environ diff --git a/library/global.ml b/library/global.ml index d5fafbb8b..a7cd61184 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/library/global.mli b/library/global.mli index 17ad57138..ae2ed16f7 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Univ open Term diff --git a/library/goptions.ml b/library/goptions.ml index 06d4b618e..e23bee15d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* This module manages customization parameters at the vernacular level *) open Pp diff --git a/library/goptions.mli b/library/goptions.mli index a8ed8a045..c63845ae0 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** This module manages customization parameters at the vernacular level *) (** Two kinds of things are managed : tables and options value diff --git a/library/heads.ml b/library/heads.ml index 056f78a5f..1f2cdc6f9 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/library/heads.mli b/library/heads.mli index bddee835f..5a0df8423 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: heads.mli 10841 2008-04-24 07:19:57Z herbelin {% $ %} *) - open Names open Term open Environ diff --git a/library/impargs.ml b/library/impargs.ml index b53b2a89d..f7d998d8c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Libnames diff --git a/library/impargs.mli b/library/impargs.mli index dc66e5493..f43880e29 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Libnames open Term diff --git a/library/lib.ml b/library/lib.ml index c8f5c6258..dcf7e70cd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Libnames diff --git a/library/lib.mli b/library/lib.mli index e8b905f26..f1e64e69a 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Sect } *) (** This module provides a general mechanism to keep a trace of all operations diff --git a/library/libnames.ml b/library/libnames.ml index 9a7135eae..13f678c5e 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/library/libnames.mli b/library/libnames.mli index 9da6a0d5c..9db6d787d 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/library/libobject.ml b/library/libobject.ml index ecdcacf1d..8577ae333 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Libnames diff --git a/library/libobject.mli b/library/libobject.mli index 8b21971aa..5a48419c9 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Libnames open Mod_subst diff --git a/library/library.ml b/library/library.ml index fbe437fc4..8677de837 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util diff --git a/library/library.mli b/library/library.mli index 05b213350..9bbb45143 100644 --- a/library/library.mli +++ b/library/library.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/library/nameops.ml b/library/nameops.ml index 28b799f53..0a0fce42b 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/library/nameops.mli b/library/nameops.mli index 414ee94ad..0f1d52420 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names (** Identifiers and names *) diff --git a/library/nametab.ml b/library/nametab.ml index c14b6cfc0..4bb9f104d 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Names diff --git a/library/nametab.mli b/library/nametab.mli index 749d00343..a464fd9a9 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Pp open Names diff --git a/library/states.ml b/library/states.ml index c4e766095..ed13c3b7a 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open System type state = Lib.frozen * Summary.frozen diff --git a/library/states.mli b/library/states.mli index fb11756e5..f0dab29f2 100644 --- a/library/states.mli +++ b/library/states.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** {6 Sect } *) (** States of the system. In that module, we provide functions to get and set the state of the whole system. Internally, it is done by diff --git a/library/summary.ml b/library/summary.ml index e9b0bbd36..b9c07ac85 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util diff --git a/library/summary.mli b/library/summary.mli index 58272aadb..0f6aaddaf 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) |