From f23e2ee0f4d64959288deea74de52fc1a4c45a22 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 May 2006 07:14:05 +0000
Subject: 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
---
 theories/FSets/FSetAVL.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 05ccff5d71..3c6f493946 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.
 
-- 
cgit v1.2.3