diff options
Diffstat (limited to 'library')
34 files changed, 34 insertions, 34 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 583ecd6f..0bb052be 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_kinds.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Libnames diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 99c07227..2d31932f 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_kinds.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Libnames diff --git a/library/declare.ml b/library/declare.ml index 630f28ed..4f5bf2bb 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: declare.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (** This module is about the low-level declaration of logical objects *) diff --git a/library/declare.mli b/library/declare.mli index dc45cf0e..f2a61180 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: declare.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/library/declaremods.ml b/library/declaremods.ml index 6a002081..ef8f2ddd 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: declaremods.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Util diff --git a/library/declaremods.mli b/library/declaremods.mli index 5045d110..51455ff6 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: declaremods.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/library/decls.ml b/library/decls.ml index db292a7e..83d5ea08 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decls.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (** This module registers tables for some non-logical informations associated declarations *) diff --git a/library/decls.mli b/library/decls.mli index 93979882..0bb66fe5 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: decls.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names open Sign diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index 1fd4d9c3..a8ee5e96 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: dischargedhypsmap.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Libnames diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index a0198f3e..77bcf2df 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: dischargedhypsmap.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Libnames diff --git a/library/global.ml b/library/global.ml index c17e3011..5139c252 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: global.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Names diff --git a/library/global.mli b/library/global.mli index 5675cf68..4290aaa0 100644 --- a/library/global.mli +++ b/library/global.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: global.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/library/goptions.ml b/library/goptions.ml index f35588b5..bfd3b272 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: goptions.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* This module manages customization parameters at the vernacular level *) diff --git a/library/goptions.mli b/library/goptions.mli index 69b09d48..d2f98cd2 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: goptions.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* This module manages customization parameters at the vernacular level *) diff --git a/library/heads.ml b/library/heads.ml index a8011206..52f98e6d 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: heads.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/library/heads.mli b/library/heads.mli index 6f3117ad..156b1307 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: heads.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Names open Term diff --git a/library/impargs.ml b/library/impargs.ml index 431e694d..2aff1dec 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: impargs.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Names diff --git a/library/impargs.mli b/library/impargs.mli index 219c75c5..1c27d9f5 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: impargs.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/library/lib.ml b/library/lib.ml index efdd0d84..fde67940 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: lib.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/library/lib.mli b/library/lib.mli index 15357708..3abe22ec 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: lib.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s This module provides a general mechanism to keep a trace of all operations diff --git a/library/libnames.ml b/library/libnames.ml index b544c8f5..d81dc60f 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: libnames.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Pp open Util diff --git a/library/libnames.mli b/library/libnames.mli index 97a49601..5dcb61ea 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: libnames.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/library/libobject.ml b/library/libobject.ml index 55a9aa08..5c7d27c6 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: libobject.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Names diff --git a/library/libobject.mli b/library/libobject.mli index 212118a8..130708aa 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: libobject.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/library/library.ml b/library/library.ml index c183e86b..c8fd89bf 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: library.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/library/library.mli b/library/library.mli index 201e5c3a..e835843d 100644 --- a/library/library.mli +++ b/library/library.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: library.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/library/nameops.ml b/library/nameops.ml index 5649fd2c..fad4f44c 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: nameops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/library/nameops.mli b/library/nameops.mli index a3fc8bdc..91434361 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: nameops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Names diff --git a/library/nametab.ml b/library/nametab.ml index 495c0062..c8d6967c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: nametab.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Pp diff --git a/library/nametab.mli b/library/nametab.mli index bb0a3323..386f3d55 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: nametab.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/library/states.ml b/library/states.ml index 972d562a..3af2bcd7 100644 --- a/library/states.ml +++ b/library/states.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: states.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open System diff --git a/library/states.mli b/library/states.mli index 35a05e9e..198e1632 100644 --- a/library/states.mli +++ b/library/states.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: states.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*s 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 63ce4c27..376f41d7 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: summary.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/library/summary.mli b/library/summary.mli index 8a7f5ed1..00301613 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: summary.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) |