- gros commit sur ring et field: passage des arguments simplifie

- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient
  pas evalues, laissant des variables libres (symptome: exc Not_found)
- reals: Open Local --> Local Open
- ListTactics: syntaxe des listes



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

9 files changed, 651 insertions, 506 deletions

diff --git a/contrib/groebner/GroebnerR.v b/contrib/groebner/GroebnerR.v
index 5f6d35d8a5..71e244126f 100644
--- a/contrib/groebner/GroebnerR.v
+++ b/contrib/groebner/GroebnerR.v
@@ -28,21 +28,17 @@
  19-12-08
 *)
 
-Require Import Reals. (* beware that Reals export Rlist *)
 Require Import List.
-Require Import ZArith.
-Require Import Znumtheory.
-Require Import List.
-Require Import Ring_polynom.
-Require Import Ring_tac.
 Require Import Setoid.
 Require Import BinPos.
 Require Import BinList.
-Require Import InitialRing.
+Require Import Znumtheory.
+Require Import Ring_polynom Ring_tac InitialRing.
+Require Import RealField Rdefinitions Rfunctions RIneq DiscrR.
 
 Declare ML Module "groebner_plugin".
 
-Open Scope R_scope.
+Local Open Scope R_scope.
 
 Lemma psos_r1b: forall x y, x - y = 0 -> x = y.
 intros x y H; replace x with ((x - y) + y);  
@@ -155,25 +151,25 @@ Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) :=
 
 (* Correction *)
 Definition PhiR : list R -> PolZ -> R := 
-  (Pphi 0%R Rplus Rmult (gen_phiZ 0%R 1%R Rplus Rmult Ropp)).
+  (Pphi 0 Rplus Rmult (gen_phiZ 0 1 Rplus Rmult Ropp)).
 
 Definition PEevalR : list R -> PEZ -> R := 
-   PEeval 0%R Rplus Rmult Rminus Ropp (gen_phiZ 0%R 1%R Rplus Rmult Ropp)
+   PEeval 0 Rplus Rmult Rminus Ropp (gen_phiZ 0 1 Rplus Rmult Ropp)
          Nnat.nat_of_N pow.
 
-Lemma P0Z_correct : forall l, PhiR l P0Z = 0%R.
+Lemma P0Z_correct : forall l, PhiR l P0Z = 0.
 Proof. trivial. Qed.
 
 
 Lemma PolZadd_correct : forall P' P l,
-  PhiR l (PolZadd P P') = (PhiR l P + PhiR l P')%R.
+  PhiR l (PolZadd P P') = (PhiR l P + PhiR l P').
 Proof.
  refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield))
            (gen_phiZ_morph Rset Rext (F_R Rfield))).
 Qed.
 
 Lemma PolZmul_correct : forall P P' l,
-  PhiR l (PolZmul P P') = (PhiR l P * PhiR l P')%R.
+  PhiR l (PolZmul P P') = (PhiR l P * PhiR l P').
 Proof.
  refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield))
            (gen_phiZ_morph Rset Rext (F_R Rfield))).
@@ -198,12 +194,12 @@ Qed.
 Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop :=
   match l with 
   | List.nil => True
-  | a::l => Interp a = 0%R /\ Cond0 A Interp l
+  | a::l => Interp a = 0 /\ Cond0 A Interp l
   end.
 
 Lemma mult_l_correct : forall l la lp, 
   Cond0 PolZ (PhiR l) lp ->
-  PhiR l (mult_l la lp) = 0%R.
+  PhiR l (mult_l la lp) = 0.
 Proof.
  induction la;simpl;intros;trivial.
  destruct lp;trivial.
@@ -224,7 +220,7 @@ Lemma check_correct :
   forall l lpe qe certif,
     check lpe qe certif = true ->
     Cond0 PEZ (PEevalR l) lpe ->
-    PEevalR l qe = 0%R.
+    PEevalR l qe = 0.
 Proof.
  unfold check;intros l lpe qe (lla, lq) H2 H1.
  apply PolZeq_correct with (l:=l) in H2.
@@ -293,20 +289,13 @@ Fixpoint interpret3 t fv {struct t}: R :=
   | (PEX n) => List.nth (pred (nat_of_P n)) fv 0
   end.
 
-Ltac AddFvTail2 a l :=
- match l with
- | (@nil _)          => constr:(cons a l)
- | (cons a _)   => l
- | (cons ?x ?l) => let l' := AddFvTail2 a l in constr:(cons x l')
- end.
-
 (* lp est incluse dans fv. La met en tete. *)
 
 Ltac parametres_en_tete fv lp :=
     match fv with
      | (@nil _)        => lp
      | (@cons _ ?x ?fv1) => 
-       let res := AddFvTail2 x lp in
+       let res := AddFvTail x lp in
          parametres_en_tete fv1 res
     end.
 
@@ -323,106 +312,77 @@ Ltac rev l :=
   end.
 
 (* Pompe sur Ring *)
-
-Ltac groebnerR_gen2 Cst_tac CstPow_tac lemma1 req n lH :=
-  let Main lhs rhs R radd rmul rsub ropp rpow C :=
-    let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in
-    let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in
-  match goal with
-  | Hparam: (@eq (@prod (@List.list ?R) (@List.list ?R)) 
-                 (?lparam, ?lvar)
-                 ?lparam2) |- _ =>
-    clear Hparam;
-    generalise_eq_hyps;
-    match goal with 
-      | |- ?t => 
-    let lpol:=lpol_goal t in
-    let rec fv_rec l lv:=
-      match l with
-       |?a::?l1 => 
-          let lv1 := mkFV a lv in
-          fv_rec l1 lv1 
-       | nil => lv
-      end in
-    let fv := 
-       match lvar with
-         | (@nil _) => let fv1 := FV_hypo_tac mkFV req lH in
-                  let fv1 := fv_rec lpol fv1 in
-                  rev fv1
-       (* heuristique: les dernieres variables auront le poid le plus fort *)
-         | _ => lvar
-      end in
-    (*let fv1 := FV_hypo_tac mkFV req lH in
-    let fv := fv_rec lpol fv1 in*)
-    check_fv fv;
-    (*idtac "variables:";idtac fv;*)
-    let nparam := eval compute in (Z_of_nat (List.length lparam)) in
-    let fv := parametres_en_tete fv lparam in
-   (* idtac "variables:"; idtac fv;
+Import Ring_tac.
+
+Ltac groebnerR_gen lparam lvar n RNG lH _rl :=
+  get_Pre RNG ();
+  let mkFV := get_RingFV RNG in
+  let mkPol := get_RingMeta RNG in
+  generalise_eq_hyps;
+  let t := Get_goal in
+  let lpol := lpol_goal t in
+  intros;
+  let fv := 
+    match lvar with
+    | nil =>
+        let fv1 := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
+        let fv1 := list_fold_right mkFV fv1 lpol in
+        rev fv1
+    (* heuristique: les dernieres variables auront le poid le plus fort *)
+    | _ => lvar
+    end in
+  check_fv fv;
+  (*idtac "variables:";idtac fv;*)
+  let nparam := eval compute in (Z_of_nat (List.length lparam)) in
+  let fv := parametres_en_tete fv lparam in
+ (* idtac "variables:"; idtac fv;
     idtac "nparam:"; idtac nparam;*)
-    let rec mkPol_list lp:=
-       match lp with
-        |?p::?lp1 => 
-            let r := mkPol p fv in
-            let lr := mkPol_list lp1 in
-            constr:(r::lr)
-        | nil =>  constr:(@nil (@PExpr Z))
-       end
-    in 
-    let lpol := mkPol_list lpol in
-    let lpol := eval compute in (List.rev lpol) in
-    let lpol := constr:((@PEc Z nparam)::lpol) in
-    (*idtac lpol;*)
-    groebner_compute lpol;
+  let lpol := list_fold_right
+    ltac:(fun p l => let p' := mkPol p fv in constr:(p'::l))
+    (@nil (PExpr Z))
+    lpol in
+  let lpol := eval compute in (List.rev lpol) in
+  let lpol := constr:(PEc nparam :: lpol) in
+  (*idtac lpol;*)
+  groebner_compute lpol;
+  let OnResult kont :=
     match goal with
-      | |- ?res=?res1 -> _ =>
-    let a1:= eval compute in lpol in
-    match a1 with
-     | ?np::?p2::?lp2 => 
-    match res with
-     | (?p ::?lp0)::(?c::?lq)::?lci => 
-       set (lci1:=lci);
-       set (lq1:=lq);
-       set (p21:=p2) ;
-       let q:= constr:(PEmul c p21) in 
-       set (q1:=q);
-       set (lp21:=lp2);
-       let Hg := fresh "Hg" in 
-     assert (Hg:check lp21 q1 (lci1,lq1) = true);
-     [vm_compute;trivial
-     |intros;
-      let Hg2 := fresh "Hg" in
-      assert (Hg2:(interpret3 q1 fv)=0);
-       [simpl; apply (@check_correct fv lp21 q1 (lci1,lq1) Hg); simpl;
-        repeat (match goal with h:_=0%R |- _ => rewrite h end);
-        repeat split; auto
-       |simpl in Hg2; simpl;
-        apply groebnerR_l3 with (interpret3 c fv);simpl;
-        [discrR; let Hc := fresh "Hg" in
-                 unfold not; intro Hc; ring_simplify in Hc;
-                 generalize Hc; clear Hc
-        |auto]
-       ]
-     ] 
-    end 
-    end 
-    end 
-  end
- end
-  in
-  ParseRingComponents lemma1 ltac:(OnEquation req Main)
-  .
-
-Ltac groebnerR_gen
-  req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl :=
-  pre();groebnerR_gen2 cst_tac pow_tac lemma1 req ring_subst_niter lH .
+    | |- (?p ::_)::(?c::?lq0)::?lci0 = _ -> _ =>
+       intros _;
+       set (lci:=lci0);
+       set (lq:=lq0);
+       kont p c lq lci
+    end in
+  let SplitPolyList kont :=
+    match lpol with
+    | _::?p2::?lp2 => kont p2 lp2
+    end in
+  OnResult ltac:(fun p c lq lci =>
+    SplitPolyList ltac:(fun p2 lp2 =>
+      set (p21:=p2) ;
+      set (lp21:=lp2);
+      set (q := PEmul c p21);
+      let Hg := fresh "Hg" in 
+      assert (Hg:check lp21 q (lci,lq) = true);
+      [ (vm_compute;reflexivity) || idtac "invalid groebner certificate"
+      | let Hg2 := fresh "Hg" in
+        assert (Hg2: interpret3 q fv = 0);
+        [ simpl; apply (@check_correct fv lp21 q (lci,lq) Hg); simpl;
+          repeat (split;[assumption|idtac]); exact I
+        | simpl in Hg2; simpl;
+          apply groebnerR_l3 with (interpret3 c fv);simpl;
+          [ discrR || idtac "could not prove discrimination result"
+          | exact Hg2]
+        ]
+      ])).
 
 Ltac groebnerRpv lparam lvar:=
   groebnerR_begin;
   intros;
-  generalize (refl_equal (lparam,lvar)); intro;
   let G := Get_goal in
-  ring_lookup groebnerR_gen [] G.
+  ring_lookup
+    (PackRing ltac:(groebnerR_gen lparam lvar ring_subst_niter))
+    [] G.
 
 Ltac groebnerR := groebnerRpv (@nil R) (@nil R).
 
@@ -438,7 +398,6 @@ Goal forall x y,
   x^2=0.
 Time groebnerR.
 Qed.
-
 Goal forall x y z u v,
   x+y+z+u+v=0 -> 
   x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index cccee60451..a88fb1ac5a 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -12,37 +12,46 @@ Require Export Field_theory.
  (* syntaxification *)
  Ltac mkFieldexpr C Cst CstPow radd rmul rsub ropp rdiv rinv rpow t fv := 
  let rec mkP t :=
+    let f :=
     match Cst t with
     | InitialRing.NotConstant =>
         match t with 
         | (radd ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(FEadd e1 e2)
         | (rmul ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(FEmul e1 e2)
         | (rsub ?t1 ?t2) => 
+          fun _ => 
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(FEsub e1 e2)
         | (ropp ?t1) =>
-          let e1 := mkP t1 in constr:(FEopp e1)
+          fun _ => let e1 := mkP t1 in constr:(FEopp e1)
         | (rdiv ?t1 ?t2) => 
+          fun _ =>
           let e1 := mkP t1 in
           let e2 := mkP t2 in constr:(FEdiv e1 e2)
         | (rinv ?t1) =>
-          let e1 := mkP t1 in constr:(FEinv e1)
+          fun _ => let e1 := mkP t1 in constr:(FEinv e1)
         | (rpow ?t1 ?n) =>
           match CstPow n with
           | InitialRing.NotConstant => 
-            let p := Find_at t fv in constr:(@FEX C p)
-          | ?c => let e1 := mkP t1 in constr:(FEpow e1 c)
+            fun _ =>
+            let p := Find_at t fv in
+            constr:(@FEX C p)
+          | ?c => fun _ => let e1 := mkP t1 in constr:(FEpow e1 c)
           end
-  
         | _ =>
-          let p := Find_at t fv in constr:(@FEX C p)
+          fun _ =>
+          let p := Find_at t fv in
+          constr:(@FEX C p)
         end
-    | ?c => constr:(FEc c)
-    end
+    | ?c => fun _ => constr:(FEc c)
+    end in
+    f ()
  in mkP t.
 
 Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
@@ -58,7 +67,8 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
       | (inv ?t1) => TFV t1 fv
       | (pow ?t1 ?n) =>
         match CstPow n with
-        | InitialRing.NotConstant => AddFvTail t fv
+        | InitialRing.NotConstant =>
+            AddFvTail t fv
         | _ => TFV t1 fv
         end
       | _ => AddFvTail t fv
@@ -67,14 +77,112 @@ Ltac FFV Cst CstPow add mul sub opp div inv pow t fv :=
   end 
  in TFV t fv.
 
-Ltac ParseFieldComponents lemma req :=
-  match type of lemma with
-  | context [
-     (*   PCond _ _ _  _ _ _ _  _ _  _ _ -> *)
-        req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv 
-                          ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
-      (fun f => f radd rmul rsub ropp rdiv rinv rpow C)
-  | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
+(* packaging the field structure *)
+
+(* TODO: inline PackField into field_lookup *)
+Ltac PackField F req Cst_tac Pow_tac L1 L2 L3 L4 cond_ok pre post :=
+  let FLD :=
+    match type of L1 with
+    | context [req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv 
+                                      ?C ?phi ?Cpow ?Cp_phi ?rpow _ _) _ ] =>
+        (fun proj =>
+           proj Cst_tac Pow_tac pre post
+             req radd rmul rsub ropp rdiv rinv rpow C L1 L2 L3 L4 cond_ok)
+    | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
+    end in
+  F FLD.
+
+Ltac get_FldPre FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       pre).
+
+Ltac get_FldPost FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       post).
+
+Ltac get_L1 FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       L1).
+
+Ltac get_SimplifyEqLemma FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       L2).
+
+Ltac get_SimplifyLemma FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       L3).
+
+Ltac get_L4 FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       L4).
+
+Ltac get_CondLemma FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       cond_ok).
+
+Ltac get_FldEq FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       req).
+
+Ltac get_FldCarrier FLD :=
+  let req := get_FldEq FLD in
+  relation_carrier req.
+
+Ltac get_RingFV FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       FV Cst_tac Pow_tac radd rmul rsub ropp rpow).
+
+Ltac get_FFV FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+
+Ltac get_RingMeta FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow).
+
+Ltac get_Meta FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow).
+
+Ltac get_Hyp_tac FLD :=
+  FLD ltac:
+      (fun Cst_tac Pow_tac pre post req radd rmul rsub ropp rdiv rinv rpow C
+           L1 L2 L3 L4 cond_ok =>
+       let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
+       fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
+
+Ltac get_FEeval FLD :=
+  let L1 := get_L1 FLD in
+  match type of L1 with
+  | context
+    [(@FEeval
+      ?R ?r0 ?add ?mul ?sub ?opp ?div ?inv ?C ?phi ?Cpow ?powphi ?pow _ _)] =>
+       constr:(@FEeval R r0 add mul sub opp div inv C phi Cpow powphi pow)
+  | _ => fail 1 "field anomaly: bad correctness lemma (get_FEeval)"
   end.
 
 (* simplifying the non-zero condition... *)
@@ -87,68 +195,72 @@ Ltac fold_field_cond req :=
     | req ?x ?y -> False => constr:(~ req x y)
     | _ => t
     end in
-  match goal with
-    |- ?t => let ft := fold_concl t in change ft
-  end.
+  let ft := fold_concl Get_goal in
+  change ft.
 
-Ltac simpl_PCond req :=
+Ltac simpl_PCond FLD :=
+  let req := get_FldEq FLD in
+  let lemma := get_CondLemma FLD in
+  try apply lemma;
   protect_fv "field_cond";
-  (try exact I);
-  fold_field_cond req.
+  fold_field_cond req;
+  try exact I.
 
-Ltac simpl_PCond_BEURK req :=
+Ltac simpl_PCond_BEURK FLD :=
+  let req := get_FldEq FLD in
+  let lemma := get_CondLemma FLD in
+  apply lemma;
   protect_fv "field_cond";
   fold_field_cond req.
 
 (* Rewriting (field_simplify) *)
-Ltac Field_norm_gen f Cst_tac Pow_tac lemma Cond_lemma req n lH rl :=
-  let Main radd rmul rsub ropp rdiv rinv rpow C :=
-    let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
-    let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
-    let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
-    let mkFE := 
-       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
-    let fv := FV_hypo_tac mkFV req lH in
-    let simpl_field H := (protect_fv "field" in H;f H) in
-    let lemma_tac fv RW_tac :=
-      let rr_lemma := fresh "f_rw_lemma" in
-      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
-      let vlpe := fresh "list_hyp" in
-      let vlmp := fresh "list_hyp_norm" in
-      let vlmp_eq := fresh "list_hyp_norm_eq" in
-      let prh := proofHyp_tac lH in
-      pose (vlpe := lpe);
-      match type of lemma with
-      | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _] =>
-        compute_assertion vlmp_eq vlmp 
-            (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe);
-         (assert (rr_lemma := lemma n vlpe fv prh vlmp vlmp_eq)
-          || fail 1 "type error when build the rewriting lemma");
-         RW_tac rr_lemma;
-        try clear rr_lemma vlmp_eq vlmp vlpe
-      | _ => fail 1 "field_simplify anomaly: bad correctness lemma"
-      end in
-    ReflexiveRewriteTactic mkFFV mkFE simpl_field lemma_tac fv rl;
-    try (apply Cond_lemma; simpl_PCond req) in
-  ParseFieldComponents lemma req Main.
-
-Ltac Field_simplify_gen f := 
-     fun req cst_tac pow_tac _ _ field_simplify_ok _ cond_ok pre post lH rl =>
-       pre(); 
-       Field_norm_gen f cst_tac pow_tac field_simplify_ok cond_ok req 
-                  ring_subst_niter lH rl; 
-      post().
+Ltac Field_norm_gen f n FLD lH rl :=
+  let mkFV := get_RingFV FLD in
+  let mkFFV := get_FFV FLD in
+  let mkFE :=  get_Meta FLD in
+  let fv0 := FV_hypo_tac mkFV ltac:(get_FldEq FLD) lH in
+  let lemma_tac fv kont :=
+    let lemma := get_SimplifyLemma FLD in
+    (* reify equations of the context *)
+    let lpe := get_Hyp_tac FLD fv lH in
+    let vlpe := fresh "hyps" in
+    pose (vlpe := lpe);
+    let prh := proofHyp_tac lH in
+    (* compute the normal form of the reified hyps *)
+    let vlmp := fresh "hyps'" in
+    let vlmp_eq := fresh "hyps_eq" in
+    let mk_monpol := get_MonPol lemma in
+    compute_assertion vlmp_eq vlmp (mk_monpol vlpe);
+    (* partially instantiate the lemma *)
+    let lem := fresh "f_rw_lemma" in
+    (assert (lem := lemma n vlpe fv prh vlmp vlmp_eq)
+     || fail "type error when building the rewriting lemma");
+    (* continuation will call main_tac for all reified terms *)
+    kont lem;
+    (* at the end, cleanup *)
+    (clear lem vlmp_eq vlmp vlpe||idtac"Field_norm_gen:cleanup failed") in
+  (* each instance of the lemma is simplified then passed to f *)
+  let main_tac H := protect_fv "field" in H; f H in
+  (* generate and use equations for each expression *)
+  ReflexiveRewriteTactic mkFFV mkFE lemma_tac main_tac fv0 rl;
+  (* simplifying the denominator condition *)
+  try simpl_PCond FLD.
+
+Ltac Field_simplify_gen f FLD lH rl := 
+  get_FldPre FLD ();
+  Field_norm_gen f ring_subst_niter FLD lH rl; 
+  get_FldPost FLD ().
 
 Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H).
 
 Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
   let G := Get_goal in
-  field_lookup Field_simplify [] rl G.
+  field_lookup (PackField Field_simplify) [] rl G.
 
 Tactic Notation (at level 0) 
   "field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
   let G := Get_goal in
-  field_lookup Field_simplify [lH] rl G.
+  field_lookup (PackField Field_simplify) [lH] rl G.
 
 Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=   
   let G := Get_goal in
@@ -156,7 +268,7 @@ Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  field_lookup Field_simplify [] rl t;
+  field_lookup (PackField Field_simplify) [] rl t;
   intro H;
   unfold g;clear g.
 
@@ -167,7 +279,7 @@ Tactic Notation "field_simplify"
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  field_lookup Field_simplify [lH] rl t;
+  field_lookup (PackField Field_simplify) [lH] rl t;
   intro H;
   unfold g;clear g.
 
@@ -188,79 +300,63 @@ Tactic Notation (at level 0)
 
 (** Generic tactic for solving equations *)
 
-Ltac Field_Scheme Simpl_tac Cst_tac Pow_tac lemma Cond_lemma req n lH :=
-  let Main radd rmul rsub ropp rdiv rinv rpow C :=
-    let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
-    let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
-    let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
-    let mkFE := 
-       mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
-    let rec ParseExpr ilemma :=
-      match type of ilemma with
-        forall nfe, ?fe = nfe -> _ =>
-          (fun t => 
-            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)
-      | _ => (fun t => t ilemma)
-      end in
-    let Main_eq t1 t2 :=
-      let fv := FV_hypo_tac mkFV req lH in
-      let fv := mkFFV t1 fv in
-      let fv := mkFFV t2 fv in
-      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
-      let prh := proofHyp_tac lH in
-      let vlpe := fresh "list_hyp" in
-      let fe1 := mkFE t1 fv in
-      let fe2 := mkFE t2 fv in
-      pose (vlpe := lpe);
-      let nlemma := fresh "field_lemma" in
-      (assert (nlemma := lemma n fv vlpe fe1 fe2 prh)
-       || fail "field anomaly:failed to build lemma"); 
-      ParseExpr nlemma
-         ltac:(fun ilemma =>
-                  apply ilemma 
-                  || fail "field anomaly: failed in applying lemma";
-                  [ Simpl_tac | apply Cond_lemma; simpl_PCond req]);
-      clear vlpe nlemma in
-    OnEquation req Main_eq in
-  ParseFieldComponents lemma req Main.
+Ltac Field_Scheme Simpl_tac n lemma FLD lH :=
+  let req := get_FldEq FLD in
+  let mkFV := get_RingFV FLD in
+  let mkFFV := get_FFV FLD in
+  let mkFE := get_Meta FLD in
+  let Main_eq t1 t2 :=
+    let fv := FV_hypo_tac mkFV req lH in
+    let fv := mkFFV t1 fv in
+    let fv := mkFFV t2 fv in
+    let lpe := get_Hyp_tac FLD fv lH in
+    let prh := proofHyp_tac lH in
+    let vlpe := fresh "list_hyp" in
+    let fe1 := mkFE t1 fv in
+    let fe2 := mkFE t2 fv in
+    pose (vlpe := lpe);
+    let nlemma := fresh "field_lemma" in
+    (assert (nlemma := lemma n fv vlpe fe1 fe2 prh)
+     || fail "field anomaly:failed to build lemma"); 
+    ProveLemmaHyps nlemma
+      ltac:(fun ilemma =>
+              apply ilemma 
+               || fail "field anomaly: failed in applying lemma";
+              [ Simpl_tac | simpl_PCond FLD]);
+    clear vlpe nlemma in
+  OnEquation req Main_eq.
 
 (* solve completely a field equation, leaving non-zero conditions to be
    proved (field) *)
 
-Ltac FIELD :=
-   let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in
-   fun req cst_tac pow_tac field_ok _ _ _ cond_ok pre post lH rl =>
-       pre(); 
-       Field_Scheme Simpl cst_tac pow_tac field_ok cond_ok req 
-         Ring_tac.ring_subst_niter lH;
-       try exact I;
-       post().
+Ltac FIELD FLD lH rl :=
+  let Simpl := vm_compute; reflexivity || fail "not a valid field equation" in
+  let lemma := get_L1 FLD in
+  get_FldPre FLD (); 
+  Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
+  try exact I;
+  get_FldPost FLD().
  
 Tactic Notation (at level 0) "field" :=
   let G := Get_goal in
-  field_lookup FIELD [] G.
+  field_lookup (PackField FIELD) [] G.
 
 Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
   let G := Get_goal in
-  field_lookup FIELD [lH] G.
+  field_lookup (PackField FIELD) [lH] G.
 
 (* transforms a field equation to an equivalent (simplified) ring equation,
    and leaves non-zero conditions to be proved (field_simplify_eq) *)
-Ltac FIELD_SIMPL  :=
+Ltac FIELD_SIMPL FLD lH rl :=
   let Simpl := (protect_fv "field") in
-  fun req cst_tac pow_tac _ field_simplify_eq_ok _ _ cond_ok pre post lH rl =>
-       pre(); 
-       Field_Scheme Simpl cst_tac pow_tac field_simplify_eq_ok cond_ok 
-          req Ring_tac.ring_subst_niter lH;
-       post().
+  let lemma := get_SimplifyEqLemma FLD in
+  get_FldPre FLD (); 
+  Field_Scheme Simpl Ring_tac.ring_subst_niter lemma FLD lH;
+  get_FldPost FLD ().
 
 Tactic Notation (at level 0) "field_simplify_eq" :=  
   let G := Get_goal in
-  field_lookup FIELD_SIMPL [] G.
+  field_lookup (PackField FIELD_SIMPL) [] G.
 
 Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=  
   let G := Get_goal in
@@ -268,62 +364,43 @@ Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=
 
 (* Same as FIELD_SIMPL but in hypothesis *)
 
-Ltac Field_simplify_eq Cst_tac Pow_tac lemma Cond_lemma req n lH :=
-   let Main radd rmul rsub ropp rdiv rinv rpow C :=
-    let hyp := fresh "hyp" in
-    intro hyp;   
-    match type of hyp with
-    | req ?t1 ?t2 =>
-      let mkFV := FV Cst_tac Pow_tac radd rmul rsub ropp rpow in
-      let mkPol := mkPolexpr C Cst_tac Pow_tac radd rmul rsub ropp rpow in
-      let mkFFV := FFV Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
-      let mkFE := 
-        mkFieldexpr C Cst_tac Pow_tac radd rmul rsub ropp rdiv rinv rpow in
-      let rec ParseExpr ilemma :=
-        match type of ilemma with
-        |  forall nfe, ?fe = nfe -> _ =>
-          (fun t => 
-            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 H x)
-        | _ => (fun t => t ilemma)
-        end in
+Ltac Field_simplify_eq n FLD lH :=
+  let req := get_FldEq FLD in
+  let mkFV := get_RingFV FLD in
+  let mkFFV := get_FFV FLD in
+  let mkFE := get_Meta FLD in
+  let lemma := get_L4 FLD in
+  let hyp := fresh "hyp" in
+  intro hyp;   
+  OnEquationHyp req hyp ltac:(fun t1 t2 =>
       let fv := FV_hypo_tac mkFV req lH in
       let fv := mkFFV t1 fv in
       let fv := mkFFV t2 fv in
-      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+      let lpe := get_Hyp_tac FLD fv lH in
       let prh := proofHyp_tac lH in
       let fe1 := mkFE t1 fv in
       let fe2 := mkFE t2 fv in
       let vlpe := fresh "vlpe" in
-      ParseExpr (lemma n fv lpe fe1 fe2 prh)
+      ProveLemmaHyps (lemma n fv lpe fe1 fe2 prh)
          ltac:(fun ilemma =>
              match type of ilemma with
              | req _ _ ->  _ -> ?EQ => 
                let tmp := fresh "tmp" in
                assert (tmp : EQ);
-               [ apply ilemma; 
-                 [ exact hyp | apply Cond_lemma; simpl_PCond_BEURK req]
-               | protect_fv "field" in tmp;
-                 generalize tmp;clear tmp ];
+               [ apply ilemma; [ exact hyp | simpl_PCond_BEURK FLD]
+               | protect_fv "field" in tmp; revert tmp ];
                clear hyp  
-             end)
-     end in
-  ParseFieldComponents lemma req Main.
+             end)).
 
-Ltac FIELD_SIMPL_EQ :=
- fun req cst_tac pow_tac _ _ _ lemma cond_ok pre post lH rl =>
-       pre(); 
-       Field_simplify_eq cst_tac pow_tac lemma cond_ok req
-         Ring_tac.ring_subst_niter lH;
-       post().
+Ltac FIELD_SIMPL_EQ FLD lH rl :=
+  get_FldPre FLD (); 
+  Field_simplify_eq Ring_tac.ring_subst_niter FLD lH;
+  get_FldPost().
 
 Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
   let t := type of H in
   generalize H;
-  field_lookup FIELD_SIMPL_EQ [] t;
+  field_lookup (PackField FIELD_SIMPL_EQ) [] t;
   [ try exact I
   | clear H;intro H].
 
@@ -332,7 +409,7 @@ Tactic Notation (at level 0)
   "field_simplify_eq" "[" constr_list(lH) "]"  "in" hyp(H) :=  
   let t := type of H in
   generalize H;
-  field_lookup FIELD_SIMPL_EQ [lH] t;
+  field_lookup (PackField FIELD_SIMPL_EQ) [lH] t;
   [ try exact I
   |clear H;intro H].
  
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index b2e5cc4b7a..fd99f786f5 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -1600,7 +1600,8 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
  match l with
    nil       => cons e nil
  | cons a l1 =>
-     if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l else cons a (Fcons0 e l1)
+     if Peq ceqb (Nnorm O nil e) (Nnorm O nil a) then l
+     else cons a (Fcons0 e l1)
  end.
  
 Theorem PFcons0_fcons_inv:
@@ -1623,6 +1624,7 @@ clear get_sign get_sign_spec.
 generalize Hp; case l0; simpl; intuition.
 Qed.
 
+(* split factorized denominators *)
 Fixpoint Fcons00 (e:PExpr C) (l:list (PExpr C)) {struct e} : list (PExpr C) :=
  match e with
    PEmul e1 e2 => Fcons00 e1 (Fcons00 e2 l)
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index 2ff3322380..53679cd5cc 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -8,14 +8,22 @@ Require Import Quote.
 Declare ML Module "newring_plugin".
   
 
-(* adds a definition id' on the normal form of t and an hypothesis id
-   stating that t = id' (tries to produces a proof as small as possible) *)
-Ltac compute_assertion id  id' t :=
-  let t' := eval vm_compute in t in
-  pose (id' := t');
-  assert (id : t = id');
-  [vm_cast_no_check (refl_equal id')|idtac].
-(* [exact_no_check (refl_equal id'<: t = id')|idtac]). *)
+(* adds a definition t' on the normal form of t and an hypothesis id
+   stating that t = t' (tries to produces a proof as small as possible) *)
+Ltac compute_assertion eqn t' t :=
+  let nft := eval vm_compute in t in
+  pose (t' := nft);
+  assert (eqn : t = t');
+  [vm_cast_no_check (refl_equal t')|idtac].
+
+Ltac relation_carrier req :=
+  let ty := type of req in
+  match eval hnf in ty with
+   ?R -> _ => R
+  | _ => fail 1000 "Equality has no relation type"
+  end.
+
+Ltac Get_goal := match goal with [|- ?G] => G end.
 
 (********************************************************************)
 (* Tacticals to build reflexive tactics *)
@@ -23,50 +31,91 @@ Ltac compute_assertion id  id' t :=
 Ltac OnEquation req :=
   match goal with
   | |- req ?lhs ?rhs => (fun f => f lhs rhs)
-  | _ => fail 1 "Goal is not an equation (of expected equality)"
+  | _ => (fun _ => fail "Goal is not an equation (of expected equality)")
+  end.
+
+Ltac OnEquationHyp req h :=
+  match type of h with
+  | req ?lhs ?rhs => fun f => f lhs rhs
+  | _ => (fun _ => fail "Hypothesis is not an equation (of expected equality)")
   end.
 
+(* Note: auxiliary subgoals in reverse order *)
 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 => tac)
+     fun kont => lapply H; [clear H; intro H; subtac kont | idtac]
+  | _ => (fun kont => kont())
   end.
 
-Ltac ApplyLemmaThen lemma expr tac :=
-  let nexpr := fresh "expr_nf" in
-  let H := fresh "eq_nf" in
-  let Heq := fresh "thm" in
-  let nf_spec :=
-    match type of (lemma expr) with
-      forall x, ?nf_spec = x -> _ => nf_spec
-    | _ => fail 1 "ApplyLemmaThen: cannot find norm expression"
-    end in
-  compute_assertion H nexpr nf_spec;
-  assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma";
-  clear H;
-  OnMainSubgoal Heq ltac:(type of Heq) ltac:(tac Heq; clear Heq nexpr).
+(* A generic pattern to have reflexive tactics do some computation:
+   lemmas of the form [forall x', x=x' -> P(x')] is understood as
+   compute the normal form of x, instantiate x' with it, prove
+   hypothesis x=x' with vm_compute and reflexivity, and pass the
+   instantiated lemma to the continuation.
+ *)
+Ltac ProveLemmaHyp lemma :=
+  match type of lemma with
+    forall x', ?x = x' -> _ =>
+      (fun kont => 
+        let x' := fresh "res" in 
+        let H := fresh "res_eq" in
+        compute_assertion H x' x;
+        let lemma' := constr:(lemma x' H) in
+        kont (lemma x' H);
+        (clear x' H||idtac"ProveLemmaHyp: cleanup failed"))
+  | _ => (fun _ => fail "ProveLemmaHyp: lemma not of the expexted form")
+  end.
 
+Ltac ProveLemmaHyps lemma := (* expects a continuation *)
+  let try_step := ProveLemmaHyp lemma in
+  (fun kont =>
+    try_step ltac:(fun lemma' => ProveLemmaHyps lemma' kont) ||
+    kont lemma).
+
+Ltac ApplyLemmaThen lemma expr kont :=
+  let lem := constr:(lemma expr) in
+  ProveLemmaHyp lem ltac:(fun lem' =>
+    let Heq := fresh "thm" in
+    assert (Heq:=lem');
+    OnMainSubgoal Heq ltac:(type of Heq) ltac:(fun _ => kont Heq);
+    (clear Heq||idtac"ApplyLemmaThen: cleanup failed")).
+(*
 Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
-  let npe := fresh "expr_nf" in
-  let H := fresh "eq_nf" in
-  let Heq := fresh "thm" in
-  let npe_spec :=
+  let pe :=
     match type of (lemma expr) with
-      forall npe, ?npe_spec = npe -> _ => npe_spec
+      forall pe', ?pe = pe' -> _ => pe
     | _ => fail 1 "ApplyLemmaThenAndCont: cannot find norm expression"
     end in
-  (compute_assertion H npe npe_spec;
-   (assert (Heq:=lemma _ _ H) || fail "anomaly: failed to apply lemma");
-   clear H;
-   OnMainSubgoal Heq ltac:(type of Heq)
-     ltac:(try tac Heq; clear Heq npe;CONT_tac cont_arg)).
+  let pe' := fresh "expr_nf" in
+  let nf_pe := fresh "pe_eq" in
+  compute_assertion nf_pe pe' pe;
+  let Heq := fresh "thm" in
+  (assert (Heq:=lemma pe pe' H) || fail "anomaly: failed to apply lemma");
+  clear nf_pe;
+  OnMainSubgoal Heq ltac:(type of Heq)
+    ltac:(try tac Heq; clear Heq pe';CONT_tac cont_arg)).
+*)
+Ltac ApplyLemmaThenAndCont lemma expr tac CONT_tac cont_arg :=
+  ApplyLemmaThen lemma expr
+    ltac:(fun lemma' => try tac lemma'; CONT_tac cont_arg).
 
 (* General scheme of reflexive tactics using of correctness lemma
-   that involves normalisation of one expression *)
-
-Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms :=
+   that involves normalisation of one expression
+   - [FV_tac term fv] is a tactic that adds the atomic expressions
+       of [term] into [fv]
+   - [SYN_tac term fv] reifies [term] given the list of atomic expressions
+   - [LEMMA_tac fv kont] computes the correctness lemma and passes it to
+       continuation kont
+   - [MAIN_tac H] process H which is the conclusion of the correctness
+       lemma instantiated with each reified term
+   - [fv] is the initial value of atomic expressions (to be completed by
+       the reification of the terms
+   - [terms] the list (a constr of type list) of terms to reify ans process.
+ *)
+Ltac ReflexiveRewriteTactic
+     FV_tac SYN_tac LEMMA_tac MAIN_tac fv terms :=
   (* extend the atom list *)
   let fv := list_fold_left FV_tac fv terms in
   let RW_tac lemma := 
@@ -79,26 +128,72 @@ Ltac ReflexiveRewriteTactic FV_tac SYN_tac MAIN_tac LEMMA_tac fv terms :=
 
 (********************************************************)
 
+Ltac FV_hypo_tac mkFV req lH :=
+  let R := relation_carrier req in
+  let FV_hypo_l_tac h :=
+    match h with @mkhypo (req ?pe _) _ => mkFV pe end in
+  let FV_hypo_r_tac h :=
+    match h with @mkhypo (req _ ?pe) _ => mkFV pe end in
+  let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in
+  list_fold_right FV_hypo_r_tac fv lH.
+
+Ltac mkHyp_tac C req Reify lH :=
+  let mkHyp h res := 
+   match h with 
+   | @mkhypo (req ?r1 ?r2) _ =>
+     let pe1 := Reify r1 in
+     let pe2 := Reify r2 in
+     constr:(cons (pe1,pe2) res)
+   | _ => fail 1 "hypothesis is not a ring equality"
+   end in
+  list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.
+
+Ltac proofHyp_tac lH :=
+  let get_proof h :=
+    match h with
+    | @mkhypo _ ?p => p
+    end in
+  let rec bh l :=
+    match l with
+    | nil => constr:(I)
+    | cons ?h nil => get_proof h
+    | cons ?h ?tl => 
+      let l := get_proof h in
+      let r := bh tl in  
+      constr:(conj l r)
+    end in
+  bh lH.
+
+Ltac get_MonPol lemma :=
+  match type of lemma with
+  | context [(mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _)] =>
+      constr:(mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb)
+  | _ => fail 1 "ring/field anomaly: bad correctness lemma (get_MonPol)"
+  end.
+
+(********************************************************)
 
 (* Building the atom list of a ring expression *)
 Ltac FV Cst CstPow add mul sub opp pow t fv :=
  let rec TFV t fv :=
+  let f :=
   match Cst t with
   | NotConstant =>
       match t with
-      | (add ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
-      | (mul ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
-      | (sub ?t1 ?t2) => TFV t2 ltac:(TFV t1 fv)
-      | (opp ?t1) => TFV t1 fv
+      | (add ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
+      | (mul ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
+      | (sub ?t1 ?t2) => fun _ => TFV t2 ltac:(TFV t1 fv)
+      | (opp ?t1) => fun _ => TFV t1 fv
       | (pow ?t1 ?n) =>
         match CstPow n with
-        | InitialRing.NotConstant => AddFvTail t fv
-        | _ => TFV t1 fv
+        | InitialRing.NotConstant => fun _ => AddFvTail t fv
+        | _ => fun _ => TFV t1 fv
         end
-      | _ => AddFvTail t fv
+      | _ => fun _ => AddFvTail t fv
       end
-  | _ => fv
-  end
+  | _ => fun _ => fv
+  end in
+  f()
  in TFV t fv.
 
  (* syntaxification of ring expressions *)
@@ -137,157 +232,160 @@ Ltac mkPolexpr C Cst CstPow radd rmul rsub ropp rpow t fv :=
     f ()
  in mkP t.
 
-Ltac ParseRingComponents lemma :=
-  match type of lemma with
-  | context [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
-      (fun f => f R add mul sub opp pow C)
-  | _ => fail 1 "ring anomaly: bad correctness lemma (parse)"
-  end.
+(* packaging the ring structure *)
+
+Ltac PackRing F req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post :=
+  let RNG :=
+    match type of lemma1 with
+    | context
+       [@PEeval ?R ?rO ?add ?mul ?sub ?opp ?C ?phi ?Cpow ?powphi ?pow _ _] =>
+        (fun proj => proj
+             cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2)
+    | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
+    end in
+  F RNG.
+
+Ltac get_Carrier RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            R).
+
+Ltac get_Eq RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            req).
+
+Ltac get_Pre RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            pre).
+
+Ltac get_Post RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            post).
+
+Ltac get_NormLemma RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            lemma1).
+
+Ltac get_SimplifyLemma RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            lemma2).
+
+Ltac get_RingFV RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            FV cst_tac pow_tac add mul sub opp pow).
+
+Ltac get_RingMeta RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+            mkPolexpr C cst_tac pow_tac add mul sub opp pow).
+
+Ltac get_RingHypTac RNG :=
+  RNG ltac:(fun cst_tac pow_tac pre post
+             R req add mul sub opp C Cpow powphi pow lemma1 lemma2 =>
+       let mkPol := mkPolexpr C cst_tac pow_tac add mul sub opp pow in
+       fun fv lH => mkHyp_tac C req ltac:(fun t => mkPol t fv) lH).
 
 (* ring tactics *)
 
-Ltac relation_carrier req :=
-  let ty := type of req in
-  match eval hnf in ty with
-   ?R -> _ => R
-  | _ => fail 1000 "Equality has no relation type"
-  end.
-
-Ltac FV_hypo_tac mkFV req lH :=
-  let R := relation_carrier req in
-  let FV_hypo_l_tac h :=
-    match h with @mkhypo (req ?pe _) _ => mkFV pe end in
-  let FV_hypo_r_tac h :=
-    match h with @mkhypo (req _ ?pe) _ => mkFV pe end in
-  let fv := list_fold_right FV_hypo_l_tac (@nil R) lH in
-  list_fold_right FV_hypo_r_tac fv lH.
-
-Ltac mkHyp_tac C req mkPE lH :=
-  let mkHyp h res := 
-   match h with 
-   | @mkhypo (req ?r1 ?r2) _ =>
-     let pe1 := mkPE r1 in
-     let pe2 := mkPE r2 in
-     constr:(cons (pe1,pe2) res)
-   | _ => fail 1 "hypothesis is not a ring equality"
-   end in
-  list_fold_right mkHyp (@nil (PExpr C * PExpr C)) lH.
-     
-Ltac proofHyp_tac lH :=
-  let get_proof h :=
-    match h with
-    | @mkhypo _ ?p => p
-    end in
-  let rec bh l :=
-    match l with
-    | nil => constr:(I)
-    | cons ?h nil => get_proof h
-    | cons ?h ?tl => 
-      let l := get_proof h in
-      let r := bh tl in  
-      constr:(conj l r)
-    end in
-  bh lH.
-
 Definition ring_subst_niter := (10*10*10)%nat.
  
-Ltac Ring Cst_tac CstPow_tac lemma1 req n lH :=
-  let Main lhs rhs R radd rmul rsub ropp rpow C :=
-    let mkFV := FV Cst_tac CstPow_tac radd rmul rsub ropp rpow in
-    let mkPol := mkPolexpr C Cst_tac CstPow_tac radd rmul rsub ropp rpow in
-    let fv := FV_hypo_tac mkFV req lH in
+Ltac Ring RNG lemma lH :=
+  let req := get_Eq RNG in
+  OnEquation req ltac:(fun lhs rhs =>
+    let mkFV := get_RingFV RNG in
+    let mkPol := get_RingMeta RNG in
+    let mkHyp := get_RingHypTac RNG in
+    let fv := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
     let fv := mkFV lhs fv in
     let fv := mkFV rhs fv in
     check_fv fv;
     let pe1 := mkPol lhs fv in
     let pe2 := mkPol rhs fv in
-    let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
+    let lpe := mkHyp fv lH in
     let vlpe := fresh "hyp_list" in
     let vfv := fresh "fv_list" in
     pose (vlpe := lpe);
     pose (vfv := fv);
-    (apply (lemma1 n vfv vlpe pe1 pe2)
+    (apply (lemma vfv vlpe pe1 pe2)
       || fail "typing error while applying ring");
     [ ((let prh := proofHyp_tac lH in exact prh)
-        || idtac "can not automatically proof hypothesis : maybe a left member of a hypothesis is not a monomial") 
+        || idtac "can not automatically proof hypothesis :";
+           idtac " maybe a left member of a hypothesis is not a monomial")
     | vm_compute;
-      (exact (refl_equal true) || fail "not a valid ring equation")] in
-  ParseRingComponents lemma1 ltac:(OnEquation req Main).
-
-Ltac Ring_norm_gen f Cst_tac CstPow_tac lemma2 req n lH rl :=
-  let Main R add mul sub opp pow C :=
-    let mkFV := FV Cst_tac CstPow_tac add mul sub opp pow in
-    let mkPol := mkPolexpr C Cst_tac CstPow_tac add mul sub opp pow in
-    let fv := FV_hypo_tac mkFV req lH in
-    let simpl_ring H := (protect_fv "ring" in H; f H) in
-    let lemma_tac fv RW_tac := 
-      let rr_lemma := fresh "r_rw_lemma" in
-      let lpe := mkHyp_tac C req ltac:(fun t => mkPol t fv) lH in
-      let vlpe := fresh "list_hyp" in
-      let vlmp := fresh "list_hyp_norm" in
-      let vlmp_eq := fresh "list_hyp_norm_eq" in
-      let prh := proofHyp_tac lH in
-      pose (vlpe := lpe);
-      match type of lemma2 with
-      | context [mk_monpol_list ?cO ?cI ?cadd ?cmul ?csub ?copp ?cdiv ?ceqb _]
-            =>
-        compute_assertion vlmp_eq vlmp 
-            (mk_monpol_list cO cI cadd cmul csub copp cdiv ceqb vlpe);
-         (assert (rr_lemma := lemma2 n vlpe fv prh vlmp vlmp_eq)
-          || fail 1 "type error when build the rewriting lemma");   
-         RW_tac rr_lemma;
-         try clear rr_lemma vlmp_eq vlmp vlpe
-      | _ => fail 1 "ring_simplify anomaly: bad correctness lemma"
-      end in
-    ReflexiveRewriteTactic mkFV mkPol simpl_ring lemma_tac fv rl in
-  ParseRingComponents lemma2 Main.
-
-
-Ltac Ring_gen
-  req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl :=
-  pre();Ring cst_tac pow_tac lemma1 req ring_subst_niter lH.
-
-Ltac Get_goal := match goal with [|- ?G] => G end.
+      (exact (refl_equal true) || fail "not a valid ring equation")]).
+
+Ltac Ring_norm_gen f RNG lemma lH rl :=
+  let mkFV := get_RingFV RNG in
+  let mkPol := get_RingMeta RNG in
+  let mkHyp := get_RingHypTac RNG in
+  let mk_monpol := get_MonPol lemma in
+  let fv := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
+  let lemma_tac fv kont := 
+    let lpe := mkHyp fv lH in
+    let vlpe := fresh "list_hyp" in
+    let vlmp := fresh "list_hyp_norm" in
+    let vlmp_eq := fresh "list_hyp_norm_eq" in
+    let prh := proofHyp_tac lH in
+    pose (vlpe := lpe);
+    compute_assertion vlmp_eq vlmp (mk_monpol vlpe);
+    let H := fresh "ring_lemma" in
+    (assert (H := lemma vlpe fv prh vlmp vlmp_eq)
+      || fail "type error when build the rewriting lemma");
+    clear vlmp_eq;
+    kont H;
+    (clear H vlmp vlpe||idtac"Ring_norm_gen: cleanup failed") in
+  let simpl_ring H := (protect_fv "ring" in H; f H) in
+  ReflexiveRewriteTactic mkFV mkPol lemma_tac simpl_ring fv rl.
+
+Ltac Ring_gen RNG lH rl :=
+  let lemma := get_NormLemma RNG in
+  get_Pre RNG ();
+  Ring RNG (lemma ring_subst_niter) lH.
 
 Tactic Notation (at level 0) "ring" :=
   let G := Get_goal in
-  ring_lookup Ring_gen [] G.
+  ring_lookup (PackRing Ring_gen) [] G.
 
 Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
   let G := Get_goal in
-  ring_lookup Ring_gen [lH] G.
+  ring_lookup (PackRing Ring_gen) [lH] G.
 
 (* Simplification *)
 
-Ltac Ring_simplify_gen f :=
-  fun req sth ext morph arth cst_tac pow_tac lemma1 lemma2 pre post lH rl =>
-     let l := fresh "to_rewrite" in
-     pose (l:= rl);
-     generalize (refl_equal l);
-     unfold l at 2;
-     pre(); 
-     let Tac RL :=
-       let Heq := fresh "Heq" in
-       intros Heq;clear Heq l;
-       Ring_norm_gen f cst_tac pow_tac lemma2 req ring_subst_niter lH RL; 
-       post() in
-     let Main :=
-       match goal with
-       | [|- l = ?RL -> _ ] => (fun f => f RL)
-       | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
-       end in
-     Main Tac.
+Ltac Ring_simplify_gen f RNG lH rl :=
+  let lemma := get_SimplifyLemma RNG in
+  let l := fresh "to_rewrite" in
+  pose (l:= rl);
+  generalize (refl_equal l);
+  unfold l at 2;
+  get_Pre RNG ();
+  let rl :=
+    match goal with
+    | [|- l = ?RL -> _ ] => RL
+    | _ => fail 1 "ring_simplify anomaly: bad goal after pre"
+    end in
+  let Heq := fresh "Heq" in
+  intros Heq;clear Heq l;
+  Ring_norm_gen f RNG (lemma ring_subst_niter) lH rl; 
+  get_Post RNG ().
 
 Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
 
 Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := 
   let G := Get_goal in
-  ring_lookup Ring_simplify [] rl G.
+  ring_lookup (PackRing Ring_simplify) [] rl G.
 
 Tactic Notation (at level 0) 
   "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
   let G := Get_goal in
-  ring_lookup Ring_simplify [lH] rl G.
+  ring_lookup (PackRing Ring_simplify) [lH] rl G.
 
 (* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
 
@@ -297,7 +395,7 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  ring_lookup Ring_simplify [] rl t;
+  ring_lookup (PackRing Ring_simplify) [] rl t;
   intro H;
   unfold g;clear g.
 
@@ -308,7 +406,7 @@ Tactic Notation
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  ring_lookup Ring_simplify [lH] rl t;
+  ring_lookup (PackRing Ring_simplify) [lH] rl t;
   intro H;
   unfold g;clear g.
 
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 2888f16f1a..095e861337 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -89,10 +89,10 @@ let interp_map l c =
 let interp_map l t =
   try Some(List.assoc t l) with Not_found -> None
 
-let protect_maps = ref ([]:(string*(constr->'a)) list)
-let add_map s m = protect_maps := (s,m) :: !protect_maps
+let protect_maps = ref Stringmap.empty
+let add_map s m = protect_maps := Stringmap.add s m !protect_maps
 let lookup_map map =
-  try List.assoc map !protect_maps
+  try Stringmap.find map !protect_maps
   with Not_found ->
     errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
 
@@ -166,14 +166,25 @@ let decl_constant na c =
       const_entry_boxed = true}, 
     IsProof Lemma))
 
+(* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
-let ltac_acall tac (args:glob_tactic_arg list) =
-  TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args)
 
+(* Calling a locally bound tactic *)
 let ltac_lcall tac args =
   TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
 
+let ltac_letin (x, e1) e2 =
+  TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
+
+let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) =
+  Tacinterp.eval_tactic
+    (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args))
+
+let ltac_record flds =
+  TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds)
+
+
 let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
 
 let dummy_goal env = 
@@ -805,14 +816,7 @@ let make_term_list carrier rl =
     (fun x l -> lapp coq_cons [|carrier;x;l|]) rl
     (lapp coq_nil [|carrier|])
 
-
-let ring_lookup (f:glob_tactic_expr) lH rl t gl =
-  let env = pf_env gl in
-  let sigma = project gl in
-  let rl = make_args_list rl t in
-  let e = find_ring_structure env sigma rl None in
-  let rl = carg (make_term_list e.ring_carrier rl) in
-  let lH = carg (make_hyp_list env lH) in
+let ltac_ring_structure e =
   let req = carg e.ring_req in
   let sth = carg e.ring_setoid in
   let ext = carg e.ring_ext in
@@ -824,12 +828,18 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
   let lemma2 = carg e.ring_lemma2 in
   let pretac = Tacexp(TacFun([None],e.ring_pre_tac)) in
   let posttac = Tacexp(TacFun([None],e.ring_post_tac)) in
-  Tacinterp.eval_tactic
-    (TacLetIn
-      (false,[(dummy_loc,id_of_string"f"),Tacexp f],
-       ltac_lcall "f"
-         [req;sth;ext;morph;th;cst_tac;pow_tac;
-          lemma1;lemma2;pretac;posttac;lH;rl])) gl
+  [req;sth;ext;morph;th;cst_tac;pow_tac;
+   lemma1;lemma2;pretac;posttac]
+
+let ring_lookup (f:glob_tactic_expr) lH rl t gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let rl = make_args_list rl t in
+  let e = find_ring_structure env sigma rl None in
+  let rl = carg (make_term_list e.ring_carrier rl) in
+  let lH = carg (make_hyp_list env lH) in
+  let ring = ltac_ring_structure e in
+  ltac_apply f (ring@[lH;rl]) gl
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
@@ -879,6 +889,11 @@ let _ = add_map "field_cond"
 (*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
 
 
+let _ = Redexpr.declare_red_expr "simpl_field_expr"
+  (protect_red "field")
+
+
+
 let afield_theory = my_constant "almost_field_theory"
 let field_theory = my_constant "field_theory"
 let sfield_theory = my_constant "semi_field_theory"
@@ -1141,13 +1156,8 @@ VERNAC COMMAND EXTEND AddSetoidField
     add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
 END
 
-let field_lookup (f:glob_tactic_expr) lH rl t gl =
-  let env = pf_env gl in
-  let sigma = project gl in
-  let rl = make_args_list rl t in
-  let e = find_field_structure env sigma rl None in
-  let rl = carg (make_term_list e.field_carrier rl) in
-  let lH = carg (make_hyp_list env lH) in
+
+let ltac_field_structure e =
   let req = carg e.field_req in
   let cst_tac = Tacexp e.field_cst_tac in
   let pow_tac = Tacexp e.field_pow_tac in
@@ -1158,14 +1168,21 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
   let cond_ok = carg e.field_cond in
   let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in
   let posttac = Tacexp(TacFun([None],e.field_post_tac)) in
-  Tacinterp.eval_tactic
-    (TacLetIn
-      (false,[(dummy_loc,id_of_string"f"),Tacexp f],
-       ltac_lcall "f"
-        [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
-         field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl
+  [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
+   field_simpl_eq_in_ok;cond_ok;pretac;posttac]
+
+let field_lookup (f:glob_tactic_expr) lH rl t gl =
+  let env = pf_env gl in
+  let sigma = project gl in
+  let rl = make_args_list rl t in
+  let e = find_field_structure env sigma rl None in
+  let rl = carg (make_term_list e.field_carrier rl) in
+  let lH = carg (make_hyp_list env lH) in
+  let field = ltac_field_structure e in
+  ltac_apply f (field@[lH;rl]) gl
+
 
 TACTIC EXTEND field_lookup
-| [ "field_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> 
+| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> 
       [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ]
 END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9df3ba4ec0..4102fae16a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2057,7 +2057,8 @@ and interp_genarg ist gl x =
       match tactic_genarg_level s with
       | Some n -> 
           (* Special treatment of tactic arguments *)
-          in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
+          in_gen (wit_tactic n)
+	    (TacArg(valueIn(val_interp ist gl (out_gen (globwit_tactic n) x))))
       | None -> 
           lookup_interp_genarg s ist gl x
 
@@ -2834,20 +2835,11 @@ let make_absolute_name ident repl =
     user_err_loc (loc,"Tacinterp.add_tacdef",
 		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
 
-let rec filter_map f l = 
-  let rec aux acc = function
-      [] -> acc
-    | hd :: tl -> 
-	match f hd with
-	    Some x -> aux (x :: acc) tl
-	  | None -> aux acc tl
-  in aux [] l
-      
 let add_tacdef isrec tacl =
   let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
   let ist =
     {(make_empty_glob_sign()) with ltacrecvars = 
-	if isrec then filter_map 
+	if isrec then list_map_filter
 	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun 
 	else []} in
   let gtacl =
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 233b40b881..017a2fe2a0 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -13,13 +13,13 @@ Require Import List.
 
 Ltac list_fold_right fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl)
+  | ?x :: ?tl => fcons x ltac:(list_fold_right fcons fnil tl)
   | nil => fnil
   end.
 
 Ltac lazy_list_fold_right fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => 
+  | ?x :: ?tl => 
        let cont := lazy_list_fold_right fcons fnil in
        fcons x cont tl
   | nil => fnil 
@@ -27,19 +27,19 @@ Ltac lazy_list_fold_right fcons fnil l :=
 
 Ltac list_fold_left fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
+  | ?x :: ?tl => list_fold_left fcons ltac:(fcons x fnil) tl
   | nil => fnil
   end.
 
 Ltac list_iter f l :=
   match l with
-  | (cons ?x ?tl) => f x; list_iter f tl
+  | ?x :: ?tl => f x; list_iter f tl
   | nil => idtac
   end.
 
 Ltac list_iter_gen seq f l :=
   match l with
-  | (cons ?x ?tl) =>
+  | ?x :: ?tl =>
       let t1 _ := f x in
       let t2 _ := list_iter_gen seq f tl in
       seq t1 t2
@@ -48,30 +48,30 @@ Ltac list_iter_gen seq f l :=
 
 Ltac AddFvTail a l :=
  match l with
- | nil          => constr:(cons a l)
- | (cons a _)   => l
- | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l')
+ | nil      => constr:(a::nil)
+ | a :: _   => l
+ | ?x :: ?l => let l' := AddFvTail a l in constr:(x::l')
  end.
 
 Ltac Find_at a l :=
  let rec find n l :=
    match l with
-   | nil => fail 100 "anomaly: Find_at"
-   | (cons a _) => eval compute in n
-   | (cons _ ?l) => find (Psucc n) l
+   | nil     => fail 100 "anomaly: Find_at"
+   | a :: _  => eval compute in n
+   | _ :: ?l => find (Psucc n) l
    end
  in find 1%positive l.
 
 Ltac check_is_list t :=
   match t with
-  | cons _ ?l => check_is_list l
-  | nil => idtac
-  | _ => fail 100 "anomaly: failed to build a canonical list"
+  | _ :: ?l => check_is_list l
+  | nil     => idtac
+  | _       => fail 100 "anomaly: failed to build a canonical list"
   end.
 
 Ltac check_fv l :=
   check_is_list l;
   match type of l with 
   | list _ => idtac
-  | _ => fail 100 "anomaly: built an ill-typed list"
+  | _      => fail 100 "anomaly: built an ill-typed list"
   end.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 8823e5d5be..55e3896a80 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -19,8 +19,8 @@ Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
 
-Open Local Scope Z_scope.
-Open Local Scope R_scope.
+Local Open Scope Z_scope.
+Local Open Scope R_scope.
 
 Implicit Type r : R.
 
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 2f69fb7616..c9f83d639a 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -19,8 +19,8 @@ Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
 Require Import Classical_Prop.
-Open Local Scope nat_scope.
-Open Local Scope R_scope.
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
 
 (** sin_PI2 is the only remaining axiom **)
 Axiom sin_PI2 : sin (PI / 2) = 1.