Changement de précédence de l'argument du by de assert; conséquences sur les .v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 7 insertions, 7 deletions

diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 7cc5230e50..8a75228bb6 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -791,7 +791,7 @@ Proof.
  exact (combine_lelistA _ H0 H1). 
  inversion_clear Hm; inversion_clear Hm'.
  constructor; auto.
- assert (lelistA (ltk (elt:=elt')) (k, e') m') by apply Inf_eq with (k',e'); auto.
+ assert (lelistA (ltk (elt:=elt')) (k, e') m') by (apply Inf_eq with (k',e'); auto).
  exact (combine_lelistA _ H0 H3). 
  inversion_clear Hm; inversion_clear Hm'.
  constructor; auto.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index a0414cd343..4645a6bbc6 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -276,7 +276,7 @@ Lemma is_empty_cardinal: is_empty s = zerob (cardinal s).
 Proof.
 intros; apply bool_1; split; intros.
 rewrite cardinal_1; simpl; auto.
-assert (cardinal s = 0) by apply zerob_true_elim; auto.
+assert (cardinal s = 0) by (apply zerob_true_elim; auto).
 auto.
 Qed.
 
@@ -672,7 +672,7 @@ unfold Add, MP.Add; intros.
 repeat rewrite filter_iff; auto.
 rewrite H0; clear H0.
 assert (E.eq x y -> f y = true) by 
- intro H0; rewrite <- (Comp _ _ H0); auto.
+ (intro H0; rewrite <- (Comp _ _ H0); auto).
 tauto.
 Qed.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 8a5156e1c6..e2a2cd45f6 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -760,8 +760,8 @@ Module Properties (M: S).
    forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
   Proof.
   assert (st := gen_st nat).
-  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by unfold compat_op; auto. 
-  assert (fp : transpose (@eq _) (fun _:elt => S)) by unfold transpose; auto.
+  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by (unfold compat_op; auto). 
+  assert (fp : transpose (@eq _) (fun _:elt => S)) by (unfold transpose; auto).
   intros s p; pattern s; apply set_induction; clear s; intros.
   rewrite (fold_1 st p (fun _ => S) H).
   rewrite (fold_1 st 0 (fun _ => S) H); trivial.
diff --git a/theories/FSets/FSetWeakProperties.v b/theories/FSets/FSetWeakProperties.v
index 44977da2ae..12a180298d 100644
--- a/theories/FSets/FSetWeakProperties.v
+++ b/theories/FSets/FSetWeakProperties.v
@@ -761,8 +761,8 @@ Module Properties (M: S).
    forall s p, fold (fun _ => S) s p = fold (fun _ => S) s 0 + p.
   Proof.
   assert (st := gen_st nat).
-  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by unfold compat_op; auto. 
-  assert (fp : transpose (@eq _) (fun _:elt => S)) by unfold transpose; auto.
+  assert (fe : compat_op E.eq (@eq _) (fun _ => S)) by (unfold compat_op; auto). 
+  assert (fp : transpose (@eq _) (fun _:elt => S)) by (unfold transpose; auto).
   intros s p; pattern s; apply set_induction; clear s; intros.
   rewrite (fold_1 st p (fun _ => S) H).
   rewrite (fold_1 st 0 (fun _ => S) H); trivial.