1 files changed, 160 insertions, 124 deletions

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 90f5f8e6..99bb8440 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -1,23 +1,25 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Ltac_plugin
 open Pp
-open CErrors
 open Util
 open Names
-open Term
+open Constr
+open EConstr
 open Vars
 open CClosure
 open Environ
 open Libnames
 open Globnames
 open Glob_term
-open Tacticals
 open Tacexpr
 open Coqlib
 open Mod_subst
@@ -31,6 +33,8 @@ open Misctypes
 open Newring_ast
 open Proofview.Notations
 
+let error msg = CErrors.user_err Pp.(str msg)
+
 (****************************************************************************)
 (* controlled reduction *)
 
@@ -42,25 +46,27 @@ 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
-    with Not_found -> anomaly (str "global_head_of_constr")
+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 -> CErrors.anomaly (str "global_head_of_constr.")
 
 let global_of_constr_nofail c = 
   try global_of_constr 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 ->
-        (match kind_of_term t with
+        (match Constr.kind t with
             App(f,args) -> mk_clos_app_but f_map subs f args 0
           | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t
           | _ -> mk_atom t)
 
 and mk_clos_app_but f_map subs f args n =
+  let open Constr in
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
     let fargs, args' = Array.chop n args in
@@ -79,11 +85,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")
+    CErrors.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) (create_tab ())
+    (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 +104,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) ] ->
@@ -121,11 +130,11 @@ let closed_term_ast l =
     mltac_name = tacname;
     mltac_index = 0;
   } in
-  let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
-  TacFun([Some(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)]))
+  let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
+  TacFun([Name(Id.of_string"t")],
+  TacML(Loc.tag (tacname,
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(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,33 +144,36 @@ 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)
-
-let decl_constant na ctx c =
-  let vars = Universes.universes_of_constr c in
-  let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
+  fst (Constrintern.interp_constr env sigma c)
+
+let decl_constant na univs c =
+  let open Constr in
+  let env = Global.env () in
+  let vars = Univops.universes_of_constr env c in
+  let univs = Univops.restrict_universe_context univs vars in
+  let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
-	    (DefinitionEntry (definition_entry ~opaque:true
-				~univs:(Univ.ContextSet.to_context ctx) c),
+            (DefinitionEntry (definition_entry ~opaque:true ~univs c),
 	     IsProof Lemma))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args))
+  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
+  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
 
 let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
   let fold arg (i, vars, lfun) =
     let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar (Loc.ghost, id)) in
+    let x = Reference (ArgVar CAst.(make id)) in
     (succ i, x :: vars, Id.Map.add id arg lfun)
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
@@ -171,11 +183,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 [||]
@@ -196,7 +208,7 @@ let get_res =
 let exec_tactic env evd n f args =
   let fold arg (i, vars, lfun) =
     let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar (Loc.ghost, id)) in
+    let x = Reference (ArgVar CAst.(make id)) in
     (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
@@ -204,13 +216,14 @@ let exec_tactic env evd n f args =
   (** Build the getter *)
   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 get_res = TacML (Loc.tag (get_res, [TacGeneric n])) 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, Evd.universe_context_set evd
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
@@ -220,7 +233,7 @@ let stdlib_modules =
   ]
 
 let coq_constant c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
+  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" stdlib_modules c))
 let coq_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
@@ -238,19 +251,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,18 +278,16 @@ let plugin_modules =
     ]
 
 let my_constant c =
-  lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
+  lazy (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Ring" plugin_modules c))
 let my_reference c =
   lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
-let new_ring_path =
-  DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let znew_ring_path =
   DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
+  lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s))
 
-let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
+let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 
 (* Ring theory *)
@@ -309,27 +320,29 @@ 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_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
-    (* PEeval: evaluate morphism and polynomial, protect ring
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+    (* PEeval: evaluate 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|10|13->Eval|8|12->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -348,15 +361,15 @@ 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"
+            CErrors.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"
+          CErrors.user_err ~hdr:"ring"
             (str"cannot find a declared ring structure over"++
-             spc()++str"\""++pr_constr ty++str"\""))
+             spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
     | [] -> assert false
 
 let add_entry (sp,_kn) e =
@@ -379,7 +392,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 &&
+     Constr.equal set' th.ring_setoid &&
      ext' == th.ring_ext &&
      morph' == th.ring_morph &&
      th' == th.ring_th &&
@@ -485,8 +498,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
@@ -517,19 +530,19 @@ let ring_equality env evd (r,add,mul,opp,req) =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
 		    Feedback.msg_info
-		    (str"Using setoid \""++pr_constr req++str"\""++spc()++
-			str"and morphisms \""++pr_constr add_m_lem ++
-			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
-			str"\""++spc()++str"and \""++pr_constr opp_m_lem++
+                    (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+                        str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
+                        str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
 			str"\"");
 		  op_morph)
             | None ->
 		(Flags.if_verbose
 		    Feedback.msg_info
-		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
-			str"and morphisms \""++pr_constr add_m_lem ++
+                    (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
 			str"\""++spc()++str"and \""++
-			pr_constr mul_m_lem++str"\"");
+                        pr_econstr_env env !evd mul_m_lem++str"\"");
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
@@ -540,15 +553,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"
 
@@ -566,8 +579,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
     | Some (Closed lc) ->
         closed_term_ast (List.map Smartlocate.global_with_alias lc)
     | None ->
-        let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
-              TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
+        let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
+              TacArg(Loc.tag (TacCall(Loc.tag (t,[]))))
 
 let make_hyp env evd c =
   let t = Retyping.get_type_of env !evd c in
@@ -581,14 +594,15 @@ 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 =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match pow with
   | None ->
-      let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|])
+      let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
+      (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
@@ -616,7 +630,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 +660,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 +710,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 +730,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,25 +744,25 @@ 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]
 
 let ring_lookup (f : Value.t) lH rl t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     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]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end
 
 (***********************************************************************)
 
@@ -748,39 +770,42 @@ let new_field_path =
   DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s))
+  lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s))
 
 
 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);
+      (function -1|9|10|11|13|15|16->Eval|12|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);
+    pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
-    (* PEeval: evaluate morphism and polynomial, protect ring
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+    (* PEeval: evaluate polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
-    (* FEeval: evaluate morphism, protect field
+    pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot);
+    (* FEeval: evaluate polynomial, 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|12|15->Eval|10|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 +820,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,15 +854,15 @@ 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"
+            CErrors.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"
+          CErrors.user_err ~hdr:"field"
             (str"cannot find a declared field structure over"++
-             spc()++str"\""++pr_constr ty++str"\""))
+             spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
     | [] -> assert false
 
 let add_field_entry (sp,_kn) e =
@@ -889,9 +915,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 +929,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 +954,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 +976,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 +1017,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,22 +1030,22 @@ 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]
 
 let field_lookup (f : Value.t) lH rl t =
-  Proofview.Goal.enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     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]))
     with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
-  end }
+  end