summaryrefslogtreecommitdiff
path: root/theories/Wellfounded
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Wellfounded')
-rw-r--r--theories/Wellfounded/Disjoint_Union.v2
-rw-r--r--theories/Wellfounded/Inclusion.v2
-rw-r--r--theories/Wellfounded/Inverse_Image.v2
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v2
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v2
-rw-r--r--theories/Wellfounded/Transitive_Closure.v2
-rw-r--r--theories/Wellfounded/Union.v2
-rw-r--r--theories/Wellfounded/Well_Ordering.v2
-rw-r--r--theories/Wellfounded/Wellfounded.v2
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.