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

9 files changed, 9 insertions, 9 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 62e0d398..7f2ea63d 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Datatypes.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 16c32b35..4c9bd919 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Logic.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Set Implicit Arguments.
 
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index d002c967..b9ea3095 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Logic_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** This module defines type constructors for types in [Type]
     ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index e8a11952..0eba44b3 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Notations.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** These are the notations whose level and associativity are imposed by Coq *)
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index e86939c8..a6f94752 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Peano.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** The type [nat] of Peano natural numbers (built from [O] and [S])
     is defined in [Datatypes.v] *)
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index d7625147..63d53560 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Prelude.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Require Export Notations.
 Require Export Logic.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 26c0194e..436a7957 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Specif.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** Basic specifications : sets that may contain logical information *)
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 3a845e6a..58920228 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Tactics.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 Require Import Notations.
 Require Import Logic.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index a7887913..be7becda 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: Wf.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (** * This module proves the validity of
     - well-founded recursion (also known as course of values)