diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-09 12:45:15 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-09 12:45:15 +0000 |
| commit | fa8272263e70535dc8db3c5e296c3635bf4139de (patch) | |
| tree | ac5b1f1aa8bd175a2eb4d9ff17afbbc0b5b54125 /theories/Relations | |
| parent | 2e43dde0f53e8aa1e0afc9d0c214825678aec481 (diff) | |
Fix a typo(?) in previous commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12382 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations')
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 6 |
1 files changed, 3 insertions, 3 deletions
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 |