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

9 files changed, 24 insertions, 18 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5f358e6944..936d960d79 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -138,7 +138,7 @@ let coqdoc_unfreeze (lt,tn,lp) =
   token_number := tn;
   last_pos := lp
 
-let add_glob loc ref = 
+let split_global ref =
   let sp = Nametab.sp_of_global ref in
   let lib_dp = Lib.library_part ref in
   let mod_dp,id = repr_path sp in
@@ -147,6 +147,12 @@ let add_glob loc ref =
   let fullname = string_of_qualid (make_qualid mod_dp_trunc id) in
   dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath fullname)
 
+let add_glob loc ref = 
+  let file,fields,id = split_global ref in
+  let filepath = string_of_dirpath file in
+  let modpath = string_of_qualid (make_qualid fields id) in
+  dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) filepath modpath)
+
 let loc_of_notation f loc args ntn =
   if args=[] or ntn.[0] <> '_' then fst (unloc loc)
   else snd (unloc (f (List.hd args)))
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d87336b816..dd04506ca1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -290,7 +290,8 @@ GEXTEND Gram
     [ [ "as"; ipat = simple_intropattern -> ipat | -> IntroAnonymous ] ]
   ;
   by_tactic:
-    [ [ IDENT "by"; tac = tactic -> TacComplete tac | -> TacId [] ] ]
+    [ [ IDENT "by"; tac = tactic_expr LEVEL "3" -> TacComplete tac
+      | -> TacId [] ] ]
   ;
   simple_tactic:
     [ [ 
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.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index f9b28be3a1..76d6ff1125 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -160,7 +160,7 @@ Proof.
  inversion_clear H0.
  constructor; auto.  
  intro.
- assert (ltA x x) by eapply SortA_InfA_InA; eauto.
+ assert (ltA x x) by (eapply SortA_InfA_InA; eauto).
  elim (ltA_not_eqA H3); auto.
 Qed.
 
@@ -330,11 +330,11 @@ destruct (H3 y); clear H3.
 destruct H6; intuition.
 swap H4; apply InA_eqA with y; auto.
 destruct H0.
-assert (InA y (x' :: s')) by rewrite H3; auto.
+assert (InA y (x' :: s')) by (rewrite H3; auto).
 inversion_clear H6; auto.
 elim H1; apply eqA_trans with y; auto.
 destruct H0.
-assert (InA y (x' :: s')) by rewrite H3; auto.
+assert (InA y (x' :: s')) by (rewrite H3; auto).
 inversion_clear H7; auto.
 elim H6; auto.
 Qed.
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 1e4673b641..e24380bffb 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -129,7 +129,7 @@ Lemma permut_nil :
  forall l, permutation l nil -> l = nil.
 Proof.
 intro l; destruct l as [ | e l ]; trivial.
-assert (In e (e::l)) by red; auto.
+assert (In e (e::l)) by (red; auto).
 intro Abs; generalize (permut_In_In _ Abs H).
 inversion 1.
 Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 264c641ac0..3a610226e2 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -451,8 +451,7 @@ destruct a; intros; simpl;
  destruct (Zdiv_eucl b (Zpos p)) as (q,r);
  intros (H0,H1); 
  rewrite inj_S in H; simpl Zabs in H; 
- (assert (H2: Zabs r < Z_of_nat n) by
-  rewrite Zabs_eq; auto with zarith);  
+ assert (H2: Zabs r < Z_of_nat n) by (rewrite Zabs_eq; auto with zarith);  
  assert (IH:=IHn r (Zpos p) H2); clear IHn; 
  simpl in IH |- *; 
  rewrite H0.
@@ -527,7 +526,7 @@ destruct (Zle_lt_or_eq _ _ H2).
 generalize (IHn _ _ (conj H4 H3)).
 intros H5 H6 H7. 
 replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto.
-assert (r = Zpos p * (-q) + b) by rewrite H1; ring.
+assert (r = Zpos p * (-q) + b) by (rewrite H1; ring).
 destruct H5; auto.
 pattern r at 1; rewrite H8.
 apply Zis_gcd_sym.
@@ -541,9 +540,9 @@ ring (Zpos p * 1); auto.
 apply Zmult_le_compat_l.
 destruct q.
 omega.
-assert (0 < Zpos p0) by compute; auto.
+assert (0 < Zpos p0) by (compute; auto).
 omega.
-assert (Zpos p * Zneg p0 < 0) by compute; auto.
+assert (Zpos p * Zneg p0 < 0) by (compute; auto).
 omega. 
 compute; intros; discriminate.
 (* r=0 *)