From 596f0f2b5ab76305447ed1ef3999fd7d9939fbef Mon Sep 17 00:00:00 2001 From: mohring Date: Wed, 30 Nov 2005 10:05:53 +0000 Subject: changement parametres inductifs dans les theories git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7630 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Relation_Operators.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 86cd92b85..b538620d1 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -25,10 +25,10 @@ Section Transitive_Closure. 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. @@ -36,11 +36,11 @@ Section Reflexive_Transitive_Closure. 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. -- cgit v1.2.3