diff options
Diffstat (limited to 'theories/Wellfounded')
-rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Inclusion.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Inverse_Image.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Union.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Wellfounded.v | 2 |
9 files changed, 9 insertions, 9 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index a3f16888..940569bd 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Disjoint_Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Disjoint_Union.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 1677659c..f596640d 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Inclusion.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Inclusion.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index f2cf1d2e..3323590e 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Inverse_Image.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Inverse_Image.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index d8a4d37c..988d2475 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lexicographic_Exponentiation.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Lexicographic_Exponentiation.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Cristina Cornes diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 8ac178fc..035c1e65 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lexicographic_Product.v,v 1.12.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Lexicographic_Product.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Authors: Bruno Barras, Cristina Cornes *) diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 2e9d497b..5bf82ffb 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Transitive_Closure.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Transitive_Closure.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 8f31ce9f..269cfd9d 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Union.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index 4a20c518..e9a18e74 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Well_Ordering.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Well_Ordering.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (** Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index 87c00b47..d5dfd072 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wellfounded.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) +(*i $Id: Wellfounded.v 5920 2004-07-16 20:01:26Z herbelin $ i*) Require Export Disjoint_Union. Require Export Inclusion. |