Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

22 files changed, 34 insertions, 34 deletions

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 98cb14e4..382b5d72 100755..100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Classical_sets.v,v 1.4.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Classical_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index a2bc781d..7e4471a0 100755..100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Constructive_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Constructive_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 9fae12f5..0b2cf3e3 100755..100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Cpo.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Cpo.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 05afc298..d71c96b0 100755..100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Ensembles.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Ensembles.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Section Ensembles.
 Variable U : Type.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 5a2e4397..47b41ec3 100755..100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Finite_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Ensembles.
 
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index 952965e8..ddbf62e4 100755..100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Finite_sets_facts.v,v 1.7.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Finite_sets_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index f58f2f81..c97aa127 100755..100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Image.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Image.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index c357e26c..806e9dde 100755..100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Infinite_sets.v,v 1.5.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Infinite_sets.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 26f29c96..cfadd81c 100755..100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Integers.v,v 1.6.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Integers.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Finite_sets.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index a308282b..cdc8520c 100755..100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Multiset.v,v 1.9.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
+(*i $Id: Multiset.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (* G. Huet 1-9-95 *)
 
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index b3e59886..9924ba66 100755..100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Partial_Order.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Partial_Order.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index af6151bf..2b6c899f 100755..100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Permut.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Permut.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (* G. Huet 1-9-95 *)
 
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index a7f5e9f4..c9a52ac2 100755..100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset.v,v 1.5.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Powerset.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Relations_1.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 05c60def..210017d4 100755..100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_Classical_facts.v,v 1.5.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Powerset_Classical_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 2c71f529..47ef2ea7 100755..100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Powerset_facts.v,v 1.8.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Powerset_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Ensembles.
 Require Export Constructive_sets.
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index e33746a9..64c4c654 100755..100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1.v,v 1.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Relations_1.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Section Relations_1.
    Variable U : Type.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 62688895..6ee7f5e2 100755..100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_1_facts.v,v 1.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Relations_1_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Relations_1.
 
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 15d3ee2d..a74102fd 100755..100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2.v,v 1.4.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Relations_2.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Relations_1.
 
@@ -32,18 +32,18 @@ Section Relations_2.
 Variable U : Type.
 Variable R : Relation U.
 
-Inductive Rstar : Relation U :=
-  | Rstar_0 : forall x:U, Rstar x x
-  | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z.
+Inductive Rstar (x:U) : U -> Prop :=
+  | Rstar_0 : Rstar x x
+  | Rstar_n : forall y z:U, R x y -> Rstar y z -> Rstar x z.
 
-Inductive Rstar1 : Relation U :=
-  | Rstar1_0 : forall x:U, Rstar1 x x
-  | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y
-  | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
+Inductive Rstar1 (x:U) : U -> Prop :=
+  | Rstar1_0 : Rstar1 x x
+  | Rstar1_1 : forall y:U, R x y -> Rstar1 x y
+  | Rstar1_n : forall y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
 
-Inductive Rplus : Relation U :=
-  | Rplus_0 : forall x y:U, R x y -> Rplus x y
-  | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z.
+Inductive Rplus (x:U) : U -> Prop :=
+  | Rplus_0 : forall y:U, R x y -> Rplus x y
+  | Rplus_n : forall y z:U, R x y -> Rplus y z -> Rplus x z.
 
 Definition Strongly_confluent : Prop :=
   forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z).
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 4c729fe7..3291f3ee 100755..100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_2_facts.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Relations_2_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 6a254819..b8c65148 100755..100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3.v,v 1.7.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Relations_3.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Relations_1.
 Require Export Relations_2.
@@ -46,9 +46,9 @@ Section Relations_3.
    
    Definition Confluent : Prop := forall x:U, confluent x.
    
-   Inductive noetherian : U -> Prop :=
+   Inductive noetherian (x: U) : Prop :=
        definition_of_noetherian :
-         forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x.
+         (forall y:U, R x y -> noetherian y) -> noetherian x.
    
    Definition Noetherian : Prop := forall x:U, noetherian x.
    
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 34322dc7..38ff9eae 100755..100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -24,7 +24,7 @@
 (* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
 (****************************************************************************)
 
-(*i $Id: Relations_3_facts.v,v 1.6.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Relations_3_facts.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Relations_1.
 Require Export Relations_1_facts.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 10d26f22..42c96191 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Uniset.v,v 1.9.2.1 2004/07/16 19:31:18 herbelin Exp $ i*)
+(*i $Id: Uniset.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (** Sets as characteristic functions *)