diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-19 22:12:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-19 22:12:33 +0000 |
| commit | b22125319bf7ba65b0c5ce00124285351277895a (patch) | |
| tree | a4e44d5e1ea71156ff3ff5ad1ec7ab5e25234678 /theories7 | |
| parent | 69491a2ef1e21fe2a3678681868f7f364058fbd0 (diff) | |
Généralisation à Type de certaines propriétés des relations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6331 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7')
| -rwxr-xr-x | theories7/Relations/Relation_Operators.v | 10 |
1 files changed, 5 insertions, 5 deletions
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). |