diff options
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. *) |