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