From fa8272263e70535dc8db3c5e296c3635bf4139de Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 9 Oct 2009 12:45:15 +0000 Subject: Fix a typo(?) in previous commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12382 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Operators_Properties.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 0f609be35..c17f5f64e 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -121,7 +121,7 @@ Section Properties. right with y; auto. right with y; auto. eapply IHIHclos_trans1; auto. - apply clos_t1n_t; auto. + apply clos_t1n_trans; auto. Qed. Lemma clos_trans_t1n_iff : forall x y, @@ -129,7 +129,7 @@ Section Properties. Proof. split. apply clos_trans_t1n. - apply clos_t1n_t. + apply clos_t1n_trans. Qed. (** Direct transitive closure vs right-step extension *) @@ -159,7 +159,7 @@ Section Properties. Proof. split. apply clos_trans_tn1. - apply clos_tn1_t. + apply clos_tn1_trans. Qed. (** Direct reflexive-transitive closure is equivalent to -- cgit v1.2.3