summaryrefslogtreecommitdiff
path: root/theories/Relations
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch)
treead89c6bb57ceee608fcba2bb3435b74e0f57919e /theories/Relations
parent018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff)
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'theories/Relations')
-rw-r--r--[-rwxr-xr-x]theories/Relations/Newman.v2
-rw-r--r--[-rwxr-xr-x]theories/Relations/Operators_Properties.v2
-rw-r--r--[-rwxr-xr-x]theories/Relations/Relation_Definitions.v2
-rw-r--r--[-rwxr-xr-x]theories/Relations/Relation_Operators.v28
-rw-r--r--[-rwxr-xr-x]theories/Relations/Relations.v2
-rw-r--r--[-rwxr-xr-x]theories/Relations/Rstar.v2
6 files changed, 19 insertions, 19 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 3cf604d8..ae914933 100755..100644
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Newman.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Newman.v 8642 2006-03-17 10:09:02Z notin $ i*)
Require Import Rstar.
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 5e0e9ec8..22a08a27 100755..100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Operators_Properties.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Operators_Properties.v 8642 2006-03-17 10:09:02Z notin $ i*)
(****************************************************************************)
(* Bruno Barras *)
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index e115b0b0..22ba7413 100755..100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Relation_Definitions.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Relation_Definitions.v 8642 2006-03-17 10:09:02Z notin $ i*)
Section Relation_Definition.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index b6359ada..edc112e5 100755..100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Relation_Operators.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Relation_Operators.v 8642 2006-03-17 10:09:02Z notin $ i*)
(****************************************************************************)
(* Bruno Barras, Cristina Cornes *)
@@ -22,31 +22,31 @@ Require Import List.
(** Some operators to build relations *)
Section Transitive_Closure.
- Variable A : Set.
+ Variable A : Type.
Variable R : relation A.
- Inductive clos_trans : A -> A -> Prop :=
- | t_step : forall x y:A, R x y -> clos_trans x y
+ Inductive clos_trans (x: A) : A -> Prop :=
+ | t_step : forall y:A, R x y -> clos_trans x y
| t_trans :
- forall x y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
+ forall y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
End Transitive_Closure.
Section Reflexive_Transitive_Closure.
- Variable A : Set.
+ Variable A : Type.
Variable R : relation A.
- Inductive clos_refl_trans : relation A :=
- | rt_step : forall x y:A, R x y -> clos_refl_trans x y
- | rt_refl : forall x:A, clos_refl_trans x x
+ Inductive clos_refl_trans (x:A) : A -> Prop:=
+ | rt_step : forall y:A, R x y -> clos_refl_trans x y
+ | rt_refl : clos_refl_trans x x
| rt_trans :
- forall x y z:A,
+ forall y z:A,
clos_refl_trans x y -> clos_refl_trans y z -> clos_refl_trans x z.
End Reflexive_Transitive_Closure.
Section Reflexive_Symetric_Transitive_Closure.
- Variable A : Set.
+ Variable A : Type.
Variable R : relation A.
Inductive clos_refl_sym_trans : relation A :=
@@ -62,7 +62,7 @@ End Reflexive_Symetric_Transitive_Closure.
Section Transposee.
- Variable A : Set.
+ Variable A : Type.
Variable R : relation A.
Definition transp (x y:A) := R y x.
@@ -70,7 +70,7 @@ End Transposee.
Section Union.
- Variable A : Set.
+ Variable A : Type.
Variables R1 R2 : relation A.
Definition union (x y:A) := R1 x y \/ R2 x y.
@@ -164,4 +164,4 @@ End Lexicographic_Exponentiation.
Hint Unfold transp union: sets v62.
Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62.
-Hint Immediate rst_sym: sets v62. \ No newline at end of file
+Hint Immediate rst_sym: sets v62.
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 6c96f14d..2df0317b 100755..100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Relations.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Relations.v 8642 2006-03-17 10:09:02Z notin $ i*)
Require Export Relation_Definitions.
Require Export Relation_Operators.
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index 7bb3ee93..4e62d73a 100755..100644
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rstar.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Rstar.v 8642 2006-03-17 10:09:02Z notin $ i*)
(** Properties of a binary relation [R] on type [A] *)