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 /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 5fd27f4675..be2e79c706 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 abc201eb15..2c04d0fdd7 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 a83a7b4b0c..68b9ca9fb8 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 1b4564d9c7..db9e1aa6d2 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 bca52c5560..42abebe866 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 17fd440240..4cbdf4ce4c 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 ac2203ccfa..7243eb0f6d 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 091ec7d995..34a96cd8b7 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 85de6ab8f1..0154f4334f 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 bc9541cf49..b264c12284 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 d5fafbb8bc..a7cd611848 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 17ad571384..ae2ed16f7a 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 06d4b618e5..e23bee15d0 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 a8ed8a0457..c63845ae08 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 056f78a5f3..1f2cdc6f94 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 bddee835f7..5a0df84237 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 b53b2a89d1..f7d998d8c0 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 dc66e5493c..f43880e29e 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 c8f5c62585..dcf7e70cd6 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 e8b905f264..f1e64e69aa 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 9a7135eae5..13f678c5e7 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 9da6a0d5c4..9db6d787d9 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 ecdcacf1d2..8577ae333b 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 8b21971aa6..5a48419c99 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 fbe437fc44..8677de837f 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 05b2133500..9bbb451434 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 28b799f530..0a0fce42be 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 414ee94ad0..0f1d52420f 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 c14b6cfc0e..4bb9f104d6 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 749d00343a..a464fd9a93 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 c4e766095b..ed13c3b7a3 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 fb11756e57..f0dab29f22 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 e9b0bbd367..b9c07ac85d 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 58272aadbe..0f6aaddaf7 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. *) |