fixed field_simplify + changed precedence of let and fun in ltac

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

8 files changed, 74 insertions, 99 deletions

diff --git a/CHANGES b/CHANGES
index fdc3885cc1..2319f1c0ac 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,11 @@
 Changes from V8.1beta to V8.1beta2
 ==================================
 
+Syntax
+
+- changed parsing precedence of let/in and fun constructions of Ltac:
+  let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
+
 Language and commands
 
 - Added sort-polymorphism for definitions in Type.
diff --git a/contrib/field/LegacyField_Tactic.v b/contrib/field/LegacyField_Tactic.v
index a52a1f205d..63d9bdda69 100644
--- a/contrib/field/LegacyField_Tactic.v
+++ b/contrib/field/LegacyField_Tactic.v
@@ -184,15 +184,15 @@ Ltac multiply mul :=
   match goal with
   |  |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
       let AzeroT := get_component Azero FT in
-      (cut (interp_ExprA FT X2 mul <> AzeroT);
-        [ intro; let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id)
-        | weak_reduce;
-           let AoneT := get_component Aone ltac:(body_of FT)
+      cut (interp_ExprA FT X2 mul <> AzeroT);
+       [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id))
+       | weak_reduce;
+          (let AoneT := get_component Aone ltac:(body_of FT)
            with AmultT := get_component Amult ltac:(body_of FT) in
-           (try
+           try
              match goal with
              |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
-             end; clear FT X2) ])
+             end; clear FT X2) ]
   end.
 
 Ltac apply_multiply FT lvar trm :=
@@ -279,7 +279,7 @@ Ltac field_gen_aux FT :=
       let lvar := build_varlist FT (AplusT X1 X2) in
       let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
       let mul := give_mult (EAplus trm1 trm2) in
-      (cut
+      cut
         (let ft := FT in
          let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
         [ compute in |- *; auto
@@ -287,10 +287,10 @@ Ltac field_gen_aux FT :=
            apply_simplif apply_assoc; multiply mul;
            [ apply_simplif apply_multiply;
               apply_simplif ltac:(apply_inverse mul);
-              let id := grep_mult in
-              clear id; weak_reduce; clear ft vm; first
-              [ inverse_test FT; legacy ring | field_gen_aux FT ]
-           | idtac ] ])
+              (let id := grep_mult in
+               clear id; weak_reduce; clear ft vm; first
+              [ inverse_test FT; legacy ring | field_gen_aux FT ])
+           | idtac ] ]
   end.
 
 Ltac field_gen FT :=
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index 91ccf2216f..786654abb9 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -93,63 +93,31 @@ Ltac Field_simplify lemma Cond_lemma req Cst_tac :=
         let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
         let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
         let simpl_field H := protect_fv "field" in H in
-        (fun f rl => (f mkFV mkFE simpl_field lemma req rl;
-                      try (apply Cond_lemma; simpl_PCond req)))
+        fun f rl => f mkFV mkFE simpl_field lemma req rl;
+                    try (apply Cond_lemma; simpl_PCond req)
     | _ => fail 1 "field anomaly: bad correctness lemma (rewr)"
     end in
   Make_tac ReflexiveRewriteTactic.
 (* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
 
 Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
-  field_lookup (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl =>
-    (pre(); Field_simplify field_simplify_ok cond_ok req cst_tac; post())).
+  field_lookup
+    (fun req cst_tac _ _ field_simplify_ok cond_ok pre post rl =>
+       pre(); Field_simplify field_simplify_ok cond_ok req cst_tac rl; post()).
 
 
 (* Generic form of field tactics *)
 Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
-  let ParseLemma :=
-    match type of lemma with
-    | forall l fe1 fe2 nfe1 nfe2, _ = nfe1 -> _ = nfe2 -> _ -> 
-      PCond _ _ _ _ _ _ _ _ _ ->
-      req (@FEeval ?R ?rO _ _ _ _ _ _ _ _ l fe1) _ =>
-        (fun f => f R rO)
-    | _ => fail 1 "field anomaly: bad correctness lemma (scheme)" 
-    end in
-  let ParseExpr2 ilemma :=
-    match type of ilemma with
-      forall nfe1 nfe2, ?fe1 = nfe1 -> ?fe2 = nfe2 -> _ => (fun f => f fe1 fe2)
-    | _ => fail 1 "field anomaly: cannot find norm expression"
-    end in
-  let Main r1 r2 R rO :=
-    let fv := FV_tac r1 (@List.nil R) in
-    let fv := FV_tac r2 fv in
-    let fe1 := SYN_tac r1 fv in
-    let fe2 := SYN_tac r2 fv in
-    ParseExpr2 (lemma fv fe1 fe2)
-    ltac:(fun nfrac_val1 nfrac_val2 =>
-          (let nfrac1 := fresh "frac1" in 
-           let norm_hyp1 := fresh "norm_frac1" in
-          (compute_assertion norm_hyp1 nfrac1 nfrac_val1;
-           let nfrac2 := fresh "frac2" in 
-           let norm_hyp2 := fresh "norm_frac2" in
-          (compute_assertion norm_hyp2 nfrac2 nfrac_val2;
-           (apply (lemma fv fe1 fe2 nfrac1 nfrac2 norm_hyp1 norm_hyp2)
-            || fail "field anomaly: failed in applying lemma");
-           [ SIMPL_tac | apply Cond_lemma; simpl_PCond req];
-           try clear nfrac1 nfrac2 norm_hyp1 norm_hyp2)))) in
-  ParseLemma ltac:(OnEquation req Main).
-
-Ltac Field_Scheme_n FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
   let R := match type of req with ?R -> _ => R end in
   let rec ParseExpr ilemma :=
     match type of ilemma with
       forall nfe, ?fe = nfe -> _ =>
         (fun t => 
-          (let x := fresh "fld_expr" in 
+           let x := fresh "fld_expr" in 
            let H := fresh "norm_fld_expr" in
-           (compute_assertion H x fe;
-            ParseExpr (ilemma x H) t;
-            try clear x H)))
+           compute_assertion H x fe;
+           ParseExpr (ilemma x H) t;
+           try clear x H)
     | _ => (fun t => t ilemma)
     end in
   let Main r1 r2 :=
@@ -159,8 +127,8 @@ Ltac Field_Scheme_n FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
     let fe2 := SYN_tac r2 fv in
     ParseExpr (lemma fv fe1 fe2)
     ltac:(fun ilemma =>
-           ((apply ilemma || fail "field anomaly: failed in applying lemma");
-           [ SIMPL_tac | apply Cond_lemma; simpl_PCond req])) in
+           apply ilemma || fail "field anomaly: failed in applying lemma";
+            [ SIMPL_tac | apply Cond_lemma; simpl_PCond req]) in
   OnEquation req Main.
 
 (* solve completely a field equation, leaving non-zero conditions to be
@@ -170,13 +138,14 @@ Ltac Field lemma Cond_lemma req Cst_tac :=
     let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
     let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
     let Simpl :=
-      vm_compute; (reflexivity || fail "not a valid field equation") in
-    Field_Scheme_n mkFV mkFE Simpl lemma Cond_lemma req in
+      vm_compute; reflexivity || fail "not a valid field equation" in
+    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
   ParseFieldComponents lemma req Main.
 
 Tactic Notation (at level 0) "field" :=
-  field_lookup (fun req cst_tac field_ok _ _ cond_ok pre post rl =>
-    (pre(); Field field_ok cond_ok req cst_tac; post())).
+  field_lookup
+    (fun req cst_tac field_ok _ _ cond_ok pre post rl =>
+       pre(); Field field_ok cond_ok req cst_tac; post()).
 
 (* transforms a field equation to an equivalent (simplified) ring equation,
    and leaves non-zero conditions to be proved (field_simplify_eq) *)
@@ -185,13 +154,14 @@ Ltac Field_simplify_eq lemma Cond_lemma req Cst_tac :=
     let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
     let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
     let Simpl := (protect_fv "field") in
-    Field_Scheme_n mkFV mkFE Simpl lemma Cond_lemma req in
+    Field_Scheme mkFV mkFE Simpl lemma Cond_lemma req in
   ParseFieldComponents lemma req Main.
 
-Tactic Notation (at level 0) "field_simplify_eq" constr_list(rl) :=
-  field_lookup (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl =>
-    (pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac;
-     post())) rl.
+Tactic Notation (at level 0) "field_simplify_eq" :=
+  field_lookup
+    (fun req cst_tac _ field_simplify_eq_ok _ cond_ok pre post rl =>
+       pre(); Field_simplify_eq field_simplify_eq_ok cond_ok req cst_tac;
+       post()).
 
 (* Adding a new field *)
 
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index ec09d4f0bc..95efde7f56 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -28,7 +28,7 @@ Ltac OnMainSubgoal H ty :=
   match ty with
   | _ -> ?ty' =>
      let subtac := OnMainSubgoal H ty' in
-     (fun tac => (lapply H; [clear H; intro H; subtac tac | idtac]))
+     fun tac => lapply H; [clear H; intro H; subtac tac | idtac]
   | _ => (fun tac => tac)
   end.
 
@@ -59,7 +59,7 @@ Ltac ReflexiveRewriteTactic FV_tac SYN_tac SIMPL_tac lemma2 req rl :=
    list_iter
      ltac:(fun r =>
        let ast := SYN_tac r fv in
-       (try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast))
+       try ApplyLemmaAndSimpl SIMPL_tac (lemma2 fv) ast)
      rl).
 
 (********************************************************)
@@ -117,18 +117,18 @@ Ltac FV Cst add mul sub opp t fv :=
       req (PEeval ?rO ?add ?mul ?sub ?opp ?phi l pe1) _ =>
         let mkFV := FV Cst_tac add mul sub opp in
         let mkPol := mkPolexpr C Cst_tac add mul sub opp in
-        (fun f => f R mkFV mkPol)
+        fun f => f R mkFV mkPol
     | _ => fail 1 "ring anomaly: bad correctness lemma"
     end in
   let Main r1 r2 R mkFV mkPol :=
     let fv := mkFV r1 (@List.nil R) in
     let fv := mkFV r2 fv in
-    (check_fv fv;
-     let pe1 := mkPol r1 fv in
+    check_fv fv;
+    (let pe1 := mkPol r1 fv in
      let pe2 := mkPol r2 fv in
-     (apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring");
+     apply (lemma1 fv pe1 pe2) || fail "typing error while applying ring";
      vm_compute;
-     (exact (refl_equal true) || fail "not a valid ring equation")) in
+     exact (refl_equal true) || fail "not a valid ring equation") in
   Make_tac ltac:(OnEquation req Main).
 
 Ltac Ring_simplify Cst_tac lemma2 req rl :=
@@ -149,12 +149,12 @@ Ltac Ring_simplify Cst_tac lemma2 req rl :=
 Tactic Notation (at level 0) "ring" :=
   ring_lookup
     (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
-       (pre(); Ring cst_tac lemma1 req)).
+       pre(); Ring cst_tac lemma1 req).
 
 Tactic Notation (at level 0) "ring_simplify" constr_list(rl) :=
   ring_lookup
     (fun req sth ext morph arth cst_tac lemma1 lemma2 pre post rl =>
-       (pre(); Ring_simplify cst_tac lemma2 req rl; post())) rl.
+       pre(); Ring_simplify cst_tac lemma2 req rl; post()) rl.
 
 (* A simple macro tactic to be prefered to ring_simplify *)
 Ltac ring_replace t1 t2 := replace t1 with t2 by ring.
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2e72784b5f..cd447e5373 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -46,20 +46,26 @@ GEXTEND Gram
   GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
 
   tactic_expr:
-    [ "5" LEFTA
+    [ "5" RIGHTA
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
+          TacFun (it,body)
+      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
+          body = tactic_expr -> TacLetRecIn (rcl,body)
+      | "let"; llc = LIST1 let_clause SEP "with"; "in";
+          u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
+      | IDENT "info"; tc = tactic_expr -> TacInfo tc ]
+      
+    | "4" LEFTA
       [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
       | ta = tactic_expr; ";"; 
 	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
 	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
 	  TacThens (ta, lta) ]
-    | "4"
-      [ ]
     | "3" RIGHTA
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
       | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
-      | IDENT "info"; tc = tactic_expr -> TacInfo tc
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
@@ -68,13 +74,7 @@ GEXTEND Gram
     | "2" RIGHTA
       [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
-          TacFun (it,body)
-      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
-          body = tactic_expr -> TacLetRecIn (rcl,body)
-      | "let"; llc = LIST1 let_clause SEP "with"; "in";
-          u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-      | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
+      [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           TacMatchContext (b,false,mrl)
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fdb0ff5032..451313be5a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -521,11 +521,11 @@ let rec pr_tacarg_using_rule pr_gen = function
 let pr_then () = str ";"
 
 let ltop = (5,E)
-let lseq = 5
+let lseq = 4
 let ltactical = 3
 let lorelse = 2
-let llet = 1
-let lfun = 1
+let llet = 5
+let lfun = 5
 let lcomplete = 1
 let labstract = 3
 let lmatch = 1
@@ -533,6 +533,7 @@ let latom = 0
 let lcall = 1
 let leval = 1
 let ltatom = 1
+let linfo = 5
 
 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
 
@@ -875,7 +876,7 @@ let rec pr_tac inherited tac =
       ltactical
   | TacInfo t ->
       hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
-      ltactical
+      linfo
   | TacOrelse (t1,t2) ->
       hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
              pr_tac (lorelse,E) t2),
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 854abdd601..44be747dad 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -789,14 +789,13 @@ Ltac reg :=
             try (change (continuity_pt aux X2) in |- *; is_cont_pt) || is_cont_pt)
     |  |- (derive_pt ?X1 ?X2 ?X3 = ?X4) =>
       let trm := eval cbv beta in (X1 AppVar) in
-        let aux := rew_term trm in
-          (intro_hyp_pt aux X2;
-            let aux2 := deriv_proof aux X2 in
-              (try
-                (replace (derive_pt X1 X2 X3) with (derive_pt aux X2 aux2);
-                  [ simplify_derive aux X2;
-                    try
-                      unfold plus_fct, minus_fct, mult_fct, div_fct, id, fct_cte,
-                        inv_fct, opp_fct in |- *; (ring || ring_simplify)
-                    | try apply pr_nu ]) || is_diff_pt))
+      let aux := rew_term trm in
+      intro_hyp_pt aux X2;
+      (let aux2 := deriv_proof aux X2 in
+       try
+         (replace (derive_pt X1 X2 X3) with (derive_pt aux X2 aux2);
+           [ simplify_derive aux X2;
+             try unfold plus_fct, minus_fct, mult_fct, div_fct, id, fct_cte,
+                        inv_fct, opp_fct in |- *; ring || ring_simplify
+           | try apply pr_nu ]) || is_diff_pt)
   end.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index e7a9e06b69..4c9470b36e 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -374,8 +374,8 @@ Module MoreInt (I:Int).
 
   Ltac omega_max_genspec x y := 
     generalize (max_spec x y); 
-      let z := fresh "z" in let Hz := fresh "Hz" in 
-	(set (z:=Zmax x y); clearbody z).
+    (let z := fresh "z" in let Hz := fresh "Hz" in 
+     set (z:=Zmax x y); clearbody z).
 
   Ltac omega_max_loop := 
     match goal with