4 files changed, 137 insertions, 125 deletions

diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 293722125b..facd2e0625 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -59,11 +59,12 @@ Notation Rset := (Eqsth R).
 Notation Rext := (Eq_ext Rplus Rmult Ropp).
 
 Lemma Rlt_0_2 : 0 < 2.
+Proof.
 apply Rlt_trans with (0 + 1).
  apply Rlt_n_Sn.
  rewrite Rplus_comm.
    apply Rplus_lt_compat_l.
-    replace 1 with (0 + 1).
+    replace R1 with (0 + 1).
   apply Rlt_n_Sn.
   apply Rplus_0_l.
 Qed.
@@ -126,9 +127,17 @@ Ltac Rpow_tac t :=
   | _ => constr:(N.of_nat t)
   end.
 
-Add Field RField : Rfield
-   (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
-
-
-
+Ltac IZR_tac t :=
+  match t with
+  | R0 => constr:(0%Z)
+  | R1 => constr:(1%Z)
+  | IZR ?u =>
+    match isZcst u with
+    | true => u
+    | _ => constr:(InitialRing.NotConstant)
+    end
+  | _ => constr:(InitialRing.NotConstant)
+  end.
 
+Add Field RField : Rfield
+   (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]).
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 216eb8b373..05ab8ab326 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Pp
 open Util
 open Libnames
@@ -15,9 +16,9 @@ open Printer
 open Newring_ast
 open Newring
 open Stdarg
-open Constrarg
+open Tacarg
 open Pcoq.Constr
-open Pcoq.Tactic
+open Pltac
 
 DECLARE PLUGIN "newring_plugin"
 
@@ -77,9 +78,7 @@ END
 
 VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
-    [ let l = match l with None -> [] | Some l -> l in
-      let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
-      add_theory id (ic t) set k cst (pre,post) power sign div]
+    [ let l = match l with None -> [] | Some l -> l in add_theory id t l]
   | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
     Feedback.msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
@@ -92,7 +91,7 @@ END
 
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
-    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t]
+    [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t ]
 END
 
 let pr_field_mod = function
@@ -114,9 +113,7 @@ END
 
 VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
-  [ let l = match l with None -> [] | Some l -> l in
-    let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods l in
-    add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign div]
+  [ let l = match l with None -> [] | Some l -> l in add_field_theory id t l ]
 | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
     Feedback.msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 90f5f8e63d..dd68eac24c 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Pp
 open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Vars
 open CClosure
 open Environ
@@ -42,9 +44,9 @@ let tag_arg tag_rec map subs i c =
     | Prot -> mk_atom c
     | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
 
-let global_head_of_constr c = 
-  let f, args = decompose_app c in
-    try global_of_constr f
+let global_head_of_constr sigma c = 
+  let f, args = decompose_app sigma c in
+    try fst (Termops.global_of_constr sigma f)
     with Not_found -> anomaly (str "global_head_of_constr")
 
 let global_of_constr_nofail c = 
@@ -52,6 +54,7 @@ let global_of_constr_nofail c =
   with Not_found -> VarRef (Id.of_string "dummy")
 
 let rec mk_clos_but f_map subs t =
+  let open Term in
   match f_map (global_of_constr_nofail t) with
     | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
     | None ->
@@ -61,6 +64,7 @@ let rec mk_clos_but f_map subs t =
           | _ -> mk_atom t)
 
 and mk_clos_app_but f_map subs f args n =
+  let open Term in
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
     let fargs, args' = Array.chop n args in
@@ -79,11 +83,13 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
   try String.Map.find map !protect_maps
   with Not_found ->
-    errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
+    user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found")
 
-let protect_red map env sigma c =
-  kl (create_clos_infos all env)
-    (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
+let protect_red map env sigma c0 =
+  let evars ev = Evarutil.safe_evar_value sigma ev in
+  let c = EConstr.Unsafe.to_constr c0 in
+  EConstr.of_constr (kl (create_clos_infos ~evars all env)
+    (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
 
 let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None
@@ -96,9 +102,10 @@ let protect_tac_in map id =
 
 let closed_term t l =
   let open Quote_plugin in
+  Proofview.tclEVARMAP >>= fun sigma ->
   let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
-  if Quote.closed_under cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+  if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 
 (* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
@@ -122,10 +129,10 @@ let closed_term_ast l =
     mltac_index = 0;
   } in
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
-  TacFun([Some(Id.of_string"t")],
+  TacFun([Name(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
-   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)]))
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+   TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
@@ -135,14 +142,16 @@ let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 let ic c =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  Constrintern.interp_open_constr env sigma c
+  let sigma, c = Constrintern.interp_open_constr env sigma c in
+  (sigma, c)
 
 let ic_unsafe c = (*FIXME remove *)
   let env = Global.env() in
   let sigma = Evd.from_env env in
-    fst (Constrintern.interp_constr env sigma c)
+    EConstr.of_constr (fst (Constrintern.interp_constr env sigma c))
 
 let decl_constant na ctx c =
+  let open Constr in
   let vars = Universes.universes_of_constr c in
   let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
   mkConst(declare_constant (Id.of_string na) 
@@ -171,11 +180,11 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
 
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
-    Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in
+    Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
   {Evd.it = gl; Evd.sigma = sigma}
 
 let constr_of v = match Value.to_constr v with
-  | Some c -> c
+  | Some c -> EConstr.Unsafe.to_constr c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
 let tactic_res = ref [||]
@@ -205,12 +214,13 @@ let exec_tactic env evd n f args =
   let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
   let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
   let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in
-  let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in
+  let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
   (** Evaluate the whole result *)
   let gl = dummy_goal env evd in
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
   let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
-    Array.map (fun x -> nf (constr_of x)) !tactic_res, snd (Evd.universe_context evd)
+  let nf c = nf (constr_of c) in
+  Array.map nf !tactic_res, snd (Evd.universe_context evd)
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
@@ -220,7 +230,7 @@ let stdlib_modules =
   ]
 
 let coq_constant c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
+  lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c))
 let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
@@ -238,19 +248,19 @@ let plapp evd f args =
   let fc = Evarutil.e_new_global evd (Lazy.force f) in
     mkApp(fc,args)
 
-let dest_rel0 t =
-  match kind_of_term t with
+let dest_rel0 sigma t =
+  match EConstr.kind sigma t with
   | App(f,args) when Array.length args >= 2 ->
       let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in
-      if closed0 rel then
+      if closed0 sigma rel then
         (rel,args.(Array.length args - 2),args.(Array.length args - 1))
       else error "ring: cannot find relation (not closed)"
   | _ -> error "ring: cannot find relation"
 
-let rec dest_rel t =
-  match kind_of_term t with
-  | Prod(_,_,c) -> dest_rel c
-  | _ -> dest_rel0 t
+let rec dest_rel sigma t =
+  match EConstr.kind sigma t with
+  | Prod(_,_,c) -> dest_rel sigma c
+  | _ -> dest_rel0 sigma t
 
 (****************************************************************************)
 (* Library linking *)
@@ -265,7 +275,7 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
+  lazy (EConstr.of_constr (Coqlib.gen_constant_in_modules "Ring" plugin_modules c))
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
@@ -309,31 +319,35 @@ let coq_mkhypo = my_reference "mkhypo"
 let coq_hypo = my_reference "hypo"
 
 (* Equality: do not evaluate but make recursive call on both sides *)
-let map_with_eq arg_map c =
-  let (req,_,_) = dest_rel c in
+let map_with_eq arg_map sigma c =
+  let (req,_,_) = dest_rel sigma c in
   interp_map
-    ((global_head_of_constr req,(function -1->Prot|_->Rec))::
+    ((global_head_of_constr sigma req,(function -1->Prot|_->Rec))::
     List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
 
-let map_without_eq arg_map _ =
+let map_without_eq arg_map _ _ =
   interp_map (List.map (fun (c,map) -> (Lazy.force c,map)) arg_map)
 
 let _ = add_map "ring"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
     (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
     pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)])
+    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
 
+let pr_constr c = pr_econstr c
+
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -348,13 +362,13 @@ let find_ring_structure env sigma l =
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
           if not (Reductionops.is_conv env sigma ty ty') then
-            errorlabstrm "ring"
+            user_err ~hdr:"ring"
               (str"arguments of ring_simplify do not have all the same type")
         in
         List.iter check cl';
-        (try ring_for_carrier ty
+        (try ring_for_carrier (EConstr.to_constr sigma ty)
         with Not_found ->
-          errorlabstrm "ring"
+          user_err ~hdr:"ring"
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
@@ -379,7 +393,7 @@ let subst_th (subst,th) =
   let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
-     eq_constr set' th.ring_setoid &&
+     Term.eq_constr set' th.ring_setoid &&
      ext' == th.ring_ext &&
      morph' == th.ring_morph &&
      th' == th.ring_th &&
@@ -485,8 +499,8 @@ let op_smorph r add mul req m1 m2 =
 (*         (setoid,op_morph) *)
 
 let ring_equality env evd (r,add,mul,opp,req) =
-  match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
+  match EConstr.kind !evd req with
+    | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
 	let setoid = plapp evd coq_eq_setoid [|r|] in
 	let op_morph =
 	  match opp with
@@ -540,15 +554,15 @@ let build_setoid_params env evd r add mul opp req eqth =
 
 let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
-  match kind_of_term th_typ with
+  match EConstr.kind sigma th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) ->
+        when eq_constr_nounivs sigma f (Lazy.force coq_almost_ring_theory) ->
           (None,r,zero,one,add,mul,Some sub,Some opp,req)
     | App(f,[|r;zero;one;add;mul;req|])
-        when eq_constr_nounivs f (Lazy.force coq_semi_ring_theory) ->
+        when eq_constr_nounivs sigma f (Lazy.force coq_semi_ring_theory) ->
         (Some true,r,zero,one,add,mul,None,None,req)
     | App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr_nounivs f (Lazy.force coq_ring_theory) ->
+        when eq_constr_nounivs sigma f (Lazy.force coq_ring_theory) ->
         (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"
 
@@ -581,6 +595,7 @@ let make_hyp_list env evd lH =
       (plapp evd coq_nil [|carrier|])
   in 
   let l' = Typing.e_solve_evars env evd l in
+  let l' = EConstr.Unsafe.to_constr l' in
     Evarutil.nf_evars_universes !evd l'
 
 let interp_power env evd pow =
@@ -616,7 +631,7 @@ let interp_div env evd div =
       plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
+let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
   check_required_library (cdir@["Ring_base"]);
   let env = Global.env() in
   let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
@@ -646,6 +661,9 @@ let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
     match post with
         Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
+  let r = EConstr.to_constr sigma r in
+  let req = EConstr.to_constr sigma req in
+  let sth = EConstr.to_constr sigma sth in
   let _ =
     Lib.add_leaf name
       (theory_to_obj
@@ -693,13 +711,18 @@ let process_ring_mods l =
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
+let add_theory id rth l =
+  let (sigma, rth) = ic rth in
+  let (k,set,cst,pre,post,power,sign, div) = process_ring_mods l in
+  add_theory0 id (sigma, rth) set k cst (pre,post) power sign div
+
 (*****************************************************************************)
 (* The tactics consist then only in a lookup in the ring database and
    call the appropriate ltac. *)
 
-let make_args_list rl t =
+let make_args_list sigma rl t =
   match rl with
-  | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2]
+  | [] -> let (_,t1,t2) = dest_rel0 sigma t in [t1;t2]
   | _ -> rl
 
 let make_term_list env evd carrier rl =
@@ -708,7 +731,7 @@ let make_term_list env evd carrier rl =
     (plapp evd coq_nil [|carrier|])
   in Typing.e_solve_evars env evd l
 
-let carg = Tacinterp.Value.of_constr
+let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =
   Tacinterp.Value.of_closure (Tacinterp.default_ist ()) expr
 
@@ -722,8 +745,8 @@ let ltac_ring_structure e =
   let pow_tac = tacarg e.ring_pow_tac in
   let lemma1 = carg e.ring_lemma1 in
   let lemma2 = carg e.ring_lemma2 in
-  let pretac = tacarg (TacFun([None],e.ring_pre_tac)) in
-  let posttac = tacarg (TacFun([None],e.ring_post_tac)) in
+  let pretac = tacarg (TacFun([Anonymous],e.ring_pre_tac)) in
+  let posttac = tacarg (TacFun([Anonymous],e.ring_post_tac)) in
   [req;sth;ext;morph;th;cst_tac;pow_tac;
    lemma1;lemma2;pretac;posttac]
 
@@ -732,10 +755,10 @@ let ring_lookup (f : Value.t) lH rl t =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try (* find_ring_strucure can raise an exception *)
+      let rl = make_args_list sigma rl t in
       let evdref = ref sigma in
-      let rl = make_args_list rl t in
       let e = find_ring_structure env sigma rl in
-      let rl = carg (make_term_list env evdref e.ring_carrier rl) in
+      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let ring = ltac_ring_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (ring@[lH;rl]))
@@ -755,12 +778,14 @@ let _ = add_map "field"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
     my_reference "display_linear",
       (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
     my_reference "display_pow_linear",
-     (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot);
+     (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
     pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
@@ -768,19 +793,20 @@ let _ = add_map "field"
           (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
+    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot);
     (* FEeval: evaluate morphism, protect field
        operations and make recursive call on the var map *)
-    my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
   (map_without_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
      coq_nil, (function -1->Eval|_ -> Prot);
-    (* PCond: evaluate morphism and denum list, protect ring
+     my_reference "IDphi", (function _->Eval);
+     my_reference "gen_phiZ", (function _->Eval);
+    (* PCond: evaluate denum list, protect ring
        operations and make recursive call on the var map *)
-     my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
-(*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
+     my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);;
 
 
 let _ = Redexpr.declare_reduction "simpl_field_expr"
@@ -795,21 +821,22 @@ let af_ar = my_reference"AF_AR"
 let f_r = my_reference"F_R"
 let sf_sr = my_reference"SF_SR"
 let dest_field env evd th_spec =
+  let open Termops in
   let th_typ = Retyping.get_type_of env !evd th_spec in
-  match kind_of_term th_typ with
+  match EConstr.kind !evd th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when is_global (Lazy.force afield_theory) f ->
+        when is_global !evd (Lazy.force afield_theory) f ->
         let rth = plapp evd af_ar
           [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when is_global (Lazy.force field_theory) f ->
+        when is_global !evd (Lazy.force field_theory) f ->
         let rth =
           plapp evd f_r
             [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in
         (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth)
     | App(f,[|r;zero;one;add;mul;div;inv;req|])
-        when is_global (Lazy.force sfield_theory) f ->
+        when is_global !evd (Lazy.force sfield_theory) f ->
         let rth = plapp evd sf_sr
           [|r;zero;one;add;mul;div;inv;req;th_spec|] in
         (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth)
@@ -828,13 +855,13 @@ let find_field_structure env sigma l =
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
           if not (Reductionops.is_conv env sigma ty ty') then
-            errorlabstrm "field"
+            user_err ~hdr:"field"
               (str"arguments of field_simplify do not have all the same type")
         in
         List.iter check cl';
-        (try field_for_carrier ty
+        (try field_for_carrier (EConstr.to_constr sigma ty)
         with Not_found ->
-          errorlabstrm "field"
+          user_err ~hdr:"field"
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
@@ -889,9 +916,11 @@ let ftheory_to_obj : field_info -> obj =
       classify_function = (fun x -> Substitute x) }
 
 let field_equality evd r inv req =
-  match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
-        mkApp(Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
+  match EConstr.kind !evd req with
+    | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
+        let c = Universes.constr_of_global (Coqlib.build_coq_eq_data()).congr in
+        let c = EConstr.of_constr c in
+        mkApp(c,[|r;r;inv|])
     | _ ->
 	let _setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req)],Some(r,Some req) in
@@ -901,15 +930,17 @@ let field_equality evd r inv req =
             error "field inverse should be declared as a morphism" in
 	  inv_m_lem
 
-let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv =
+let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+  let open Constr in
   check_required_library (cdir@["Field_tac"]);
+  let (sigma,fth) = ic fth in
   let env = Global.env() in
   let evd = ref sigma in
   let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
     dest_field env evd fth in
   let (sth,ext) = build_setoid_params env evd r add mul opp req eqth in
   let eqth = Some(sth,ext) in
-  let _ = add_theory name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
+  let _ = add_theory0 name (!evd,rth) eqth morphth cst_tac (None,None) power sign odiv in
   let (pow_tac, pspec) = interp_power env evd power in
   let sspec = interp_sign env evd sign in
   let dspec = interp_div env evd odiv in
@@ -924,7 +955,7 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
   let lemma4 = params.(6) in
   let cond_lemma =
     match inj with
-      | Some thm -> mkApp(params.(8),[|thm|])
+      | Some thm -> mkApp(params.(8),[|EConstr.to_constr sigma thm|])
       | None -> params.(7) in
   let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
     ctx lemma1 in
@@ -946,6 +977,8 @@ let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power
     match post with
         Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
+  let r = EConstr.to_constr sigma r in
+  let req = EConstr.to_constr sigma req in
   let _ =
     Lib.add_leaf name
       (ftheory_to_obj
@@ -985,6 +1018,10 @@ let process_field_mods l =
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
+let add_field_theory id t mods =
+  let (k,set,inj,cst_tac,pre,post,power,sign,div) = process_field_mods mods in
+  add_field_theory0 id t set k cst_tac inj (pre,post) power sign div
+
 let ltac_field_structure e =
   let req = carg e.field_req in
   let cst_tac = tacarg e.field_cst_tac in
@@ -994,8 +1031,8 @@ let ltac_field_structure e =
   let field_simpl_eq_ok = carg e.field_simpl_eq_ok in
   let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in
   let cond_ok = carg e.field_cond in
-  let pretac = tacarg (TacFun([None],e.field_pre_tac)) in
-  let posttac = tacarg (TacFun([None],e.field_post_tac)) in
+  let pretac = tacarg (TacFun([Anonymous],e.field_pre_tac)) in
+  let posttac = tacarg (TacFun([Anonymous],e.field_post_tac)) in
   [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;
    field_simpl_eq_in_ok;cond_ok;pretac;posttac]
 
@@ -1004,10 +1041,10 @@ let field_lookup (f : Value.t) lH rl t =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     try
+      let rl = make_args_list sigma rl t in
       let evdref = ref sigma in
-      let rl = make_args_list rl t in
       let e = find_field_structure env sigma rl in
-      let rl = carg (make_term_list env evdref e.field_carrier rl) in
+      let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
       let lH = carg (make_hyp_list env evdref lH) in
       let field = ltac_field_structure e in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (ltac_apply f (field@[lH;rl]))
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index f417c87cde..4367d021c0 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Constr
+open EConstr
 open Libnames
 open Globnames
 open Constrexpr
@@ -19,28 +20,12 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic
 
 val protect_tac : string -> unit Proofview.tactic
 
-val closed_term : constr -> global_reference list -> unit Proofview.tactic
-
-val process_ring_mods :
-  constr_expr ring_mod list ->
-  constr coeff_spec * (constr * constr) option *
-  cst_tac_spec option * raw_tactic_expr option *
-  raw_tactic_expr option *
-  (cst_tac_spec * constr_expr) option *
-  constr_expr option * constr_expr option
+val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic
 
 val add_theory :
   Id.t ->
-  Evd.evar_map * constr ->
-  (constr * constr) option ->
-  constr coeff_spec ->
-  cst_tac_spec option ->
-  raw_tactic_expr option * raw_tactic_expr option ->
-  (cst_tac_spec * constr_expr) option ->
-  constr_expr option ->
-  constr_expr option -> unit
-
-val ic : constr_expr -> Evd.evar_map * constr
+  constr_expr ->
+  constr_expr ring_mod list -> unit
 
 val from_name : ring_info Spmap.t ref
 
@@ -49,26 +34,10 @@ val ring_lookup :
   constr list ->
   constr list -> constr -> unit Proofview.tactic
 
-val process_field_mods :
-  constr_expr field_mod list ->
-  constr coeff_spec *
-  (constr * constr) option * constr option *
-  cst_tac_spec option * raw_tactic_expr option *
-  raw_tactic_expr option *
-  (cst_tac_spec * constr_expr) option *
-  constr_expr option * constr_expr option
-
 val add_field_theory :
   Id.t ->
-  Evd.evar_map * constr ->
-  (constr * constr) option ->
-  constr coeff_spec ->
-  cst_tac_spec option ->
-  constr option ->
-  raw_tactic_expr option * raw_tactic_expr option ->
-  (cst_tac_spec * constr_expr) option ->
-  constr_expr option ->
-  constr_expr option -> unit
+  constr_expr ->
+  constr_expr field_mod list -> unit
 
 val field_from_name : field_info Spmap.t ref