diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-24 07:14:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-24 07:14:05 +0000 |
| commit | f23e2ee0f4d64959288deea74de52fc1a4c45a22 (patch) | |
| tree | ad872b6def287b3b6bc359a071c6a0faba330ea9 /theories/FSets/FSetAVL.v | |
| parent | 259252f2d9477cd721a4a2ad29f9a6fde2bd01ca (diff) | |
Suite changement précédence by de assert
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8860 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetAVL.v')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 05ccff5d7..3c6f49394 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -939,7 +939,7 @@ Proof. inversion_clear 1. destruct t0. inversion 1; subst. - assert (X.lt x y) by apply H3; auto. + assert (X.lt x y) by (apply H3; auto). inversion_clear 1; auto; order. assert (X.lt t1 y) by auto. inversion_clear 2; auto; @@ -986,7 +986,7 @@ Proof. inversion_clear 1. destruct t2. inversion 1; subst. - assert (X.lt y x) by apply H4; auto. + assert (X.lt y x) by (apply H4; auto). inversion_clear 1; auto; order. assert (X.lt y t1) by auto. inversion_clear 2; auto; @@ -2064,7 +2064,7 @@ Proof. clear H; right; red; firstorder. clear H; right; red; inv bst; intuition. apply n; red; intros. - assert (In a (Node l2 x2 r2 h2)) by inv In; auto. + assert (In a (Node l2 x2 r2 h2)) by (inv In; auto). intuition_in; order. (* x1 = x2 *) case (H l1 l2); inv bst; auto; intros. @@ -2090,7 +2090,7 @@ Proof. clear H; right; red; firstorder. clear H; right; red; inv bst; intuition. apply n; red; intros. - assert (In a (Node l2 x2 r2 h2)) by inv In; auto. + assert (In a (Node l2 x2 r2 h2)) by (inv In; auto). intuition_in; order. Qed. |