Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

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