diff options
-rwxr-xr-x | theories/Relations/Relation_Operators.v | 12 | ||||
-rwxr-xr-x | theories7/Relations/Relation_Operators.v | 10 |
2 files changed, 11 insertions, 11 deletions
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 1933655c9..86cd92b85 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -22,7 +22,7 @@ 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 := @@ -33,7 +33,7 @@ End Transitive_Closure. Section Reflexive_Transitive_Closure. - Variable A : Set. + Variable A : Type. Variable R : relation A. Inductive clos_refl_trans : relation A := @@ -46,7 +46,7 @@ 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/theories7/Relations/Relation_Operators.v b/theories7/Relations/Relation_Operators.v index 5abedb633..500cfa117 100755 --- a/theories7/Relations/Relation_Operators.v +++ b/theories7/Relations/Relation_Operators.v @@ -23,7 +23,7 @@ Require PolyListSyntax. (** Some operators to build relations *) Section Transitive_Closure. - Variable A: Set. + Variable A: Type. Variable R: (relation A). Inductive clos_trans : A->A->Prop := @@ -33,7 +33,7 @@ End Transitive_Closure. Section Reflexive_Transitive_Closure. - Variable A: Set. + Variable A: Type. Variable R: (relation A). Inductive clos_refl_trans: (relation A) := @@ -45,7 +45,7 @@ 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) := @@ -58,7 +58,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). @@ -66,7 +66,7 @@ End Transposee. Section Union. - Variable A: Set. + Variable A: Type. Variable R1,R2: (relation A). Definition union := [x,y:A](R1 x y)\/(R2 x y). |