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

3 files changed, 42 insertions, 72 deletions

diff --git a/contrib/field/LegacyField_Tactic.v b/contrib/field/LegacyField_Tactic.v
index a52a1f205..63d9bdda6 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 91ccf2216..786654abb 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 ec09d4f0b..95efde7f5 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.