1 files changed, 339 insertions, 345 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index d1a5c0ab..2f9e8509 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -1,30 +1,27 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
+open Vars
 open Closure
 open Environ
 open Libnames
-open Tactics
+open Globnames
 open Glob_term
 open Tacticals
 open Tacexpr
-open Pcoq
-open Tactic
-open Constr
-open Proof_type
 open Coqlib
-open Tacmach
 open Mod_subst
 open Tacinterp
 open Libobject
@@ -32,14 +29,20 @@ open Printer
 open Declare
 open Decl_kinds
 open Entries
+open Misctypes
+
+DECLARE PLUGIN "newring_plugin"
 
 (****************************************************************************)
 (* controlled reduction *)
 
-let mark_arg i c = mkEvar(i,[|c|])
+(** ppedrot: something dubious here, we're obviously using evars the wrong
+    way. FIXME! *)
+
+let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|])
 let unmark_arg f c =
   match destEvar c with
-    | (i,[|c|]) -> f i c
+    | (i,[|c|]) -> f (Evar.repr i) c
     | _ -> assert false
 
 type protect_flag = Eval|Prot|Rec
@@ -48,10 +51,19 @@ let tag_arg tag_rec map subs i c =
   match map i with
       Eval -> mk_clos subs c
     | Prot -> mk_atom c
-    | Rec -> if i = -1 then mk_clos subs c else tag_rec 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_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 =
-  match f_map t with
+  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
@@ -62,9 +74,9 @@ let rec mk_clos_but f_map subs t =
 and mk_clos_app_but f_map subs f args n =
   if n >= Array.length args then mk_atom(mkApp(f, args))
   else
-    let fargs, args' = array_chop n args in
+    let fargs, args' = Array.chop n args in
     let f' = mkApp(f,fargs) in
-    match f_map f' with
+    match f_map (global_of_constr_nofail f') with
         Some map ->
           mk_clos_deep
             (fun s' -> unmark_arg (tag_arg (mk_clos_but f_map s') map s'))
@@ -72,24 +84,13 @@ and mk_clos_app_but f_map subs f args n =
             (mkApp (mark_arg (-1) f', Array.mapi mark_arg args'))
       | None -> mk_clos_app_but f_map subs f args (n+1)
 
-
-let interp_map l c =
-  try
-    let (im,am) = List.assoc c l in
-    Some(fun i ->
-      if List.mem i im then Eval
-      else if List.mem i am then Prot
-      else if i = -1 then Eval
-      else Rec)
-  with Not_found -> None
-
 let interp_map l t =
-  try Some(list_assoc_f eq_constr t l) with Not_found -> None
+  try Some(List.assoc_f eq_gr t l) with Not_found -> None
 
-let protect_maps = ref Stringmap.empty
-let add_map s m = protect_maps := Stringmap.add s m !protect_maps
+let protect_maps = ref String.Map.empty
+let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
-  try Stringmap.find map !protect_maps
+  try String.Map.find map !protect_maps
   with Not_found ->
     errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
 
@@ -101,112 +102,120 @@ let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Termops.InHyp));;
+  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));;
 
 
 TACTIC EXTEND protect_fv
   [ "protect_fv" string(map) "in" ident(id) ] ->
-    [ protect_tac_in map id ]
+    [ Proofview.V82.tactic (protect_tac_in map id) ]
 | [ "protect_fv" string(map) ] ->
-    [ protect_tac map ]
+    [ Proofview.V82.tactic (protect_tac map) ]
 END;;
 
 (****************************************************************************)
 
 let closed_term t l =
-  let l = List.map constr_of_global l in
+  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 tclIDTAC else tclFAIL 0 (mt())
 ;;
 
 TACTIC EXTEND closed_term
   [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term t l ]
+    [ Proofview.V82.tactic (closed_term t l) ]
 END
 ;;
 
-TACTIC EXTEND echo
+(* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
   [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
-END;;
+END;;*)
 
 (*
 let closed_term_ast l =
-  TacFun([Some(id_of_string"t")],
-  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
-  [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t"));
-   Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l])))
+  TacFun([Some(Id.of_string"t")],
+  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
+  [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
+   Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
 *)
 let closed_term_ast l =
-  let l = List.map (fun gr -> ArgArg(dummy_loc,gr)) l in
-  TacFun([Some(id_of_string"t")],
-  TacAtom(dummy_loc,TacExtend(dummy_loc,"closed_term",
-  [Genarg.in_gen Genarg.globwit_constr (GVar(dummy_loc,id_of_string"t"),None);
-   Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
+  let tacname = {
+    mltac_plugin = "newring_plugin";
+    mltac_tactic = "closed_term";
+  } in
+  let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
+  TacFun([Some(Id.of_string"t")],
+  TacML(Loc.ghost,tacname,
+  [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None);
+   Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l]))
 (*
-let _ = add_tacdef false ((dummy_loc,id_of_string"ring_closed_term"
+let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
 
 (****************************************************************************)
 
 let ic c =
   let env = Global.env() and sigma = Evd.empty in
-  Constrintern.interp_constr sigma env c
+  Constrintern.interp_open_constr env sigma c
+
+let ic_unsafe c = (*FIXME remove *)
+  let env = Global.env() and sigma = Evd.empty in
+    fst (Constrintern.interp_constr env sigma c)
 
 let ty c = Typing.type_of (Global.env()) Evd.empty c
 
-let decl_constant na c =
-  mkConst(declare_constant (id_of_string na) (DefinitionEntry
-    { const_entry_body = c;
-      const_entry_secctx = None;
-      const_entry_type = None;
-      const_entry_opaque = true },
-    IsProof Lemma))
+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
+  mkConst(declare_constant (Id.of_string na) 
+	    (DefinitionEntry (definition_entry ~opaque:true
+				~univs:(Univ.ContextSet.to_context ctx) c),
+	     IsProof Lemma))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
 
 let ltac_letin (x, e1) e2 =
-  TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
+  TacLetIn(false,[(Loc.ghost,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)
+  TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
 
 
-let carg c = TacDynamic(dummy_loc,Pretyping.constr_in c)
+let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
 
-let dummy_goal env =
+let dummy_goal env sigma =
   let (gl,_,sigma) = 
-    Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
-  {Evd.it = gl;
-   Evd.sigma = sigma}
+    Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in
+  {Evd.it = gl; Evd.sigma = sigma}
 
-let exec_tactic env n f args =
-  let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
+let constr_of v = match Value.to_constr v with
+  | Some c -> c
+  | None -> failwith "Ring.exec_tactic: anomaly"
+
+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 res = ref [||] in
   let get_res ist =
-    let l = List.map (fun id ->  List.assoc id ist.lfun) lid in
+    let l = List.map (fun id ->  Id.Map.find id ist.lfun) lid in
     res := Array.of_list l;
     TacId[] in
   let getter =
     Tacexp(TacFun(List.map(fun id -> Some id) lid,
-                  glob_tactic(tacticIn get_res))) in
-  let _ =
-    Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
-  !res
-
-let constr_of = function
-  | VConstr ([],c) -> c
-  | _ -> failwith "Ring.exec_tactic: anomaly"
+                  Tacintern.glob_tactic(tacticIn get_res))) in
+  let gl = dummy_goal env evd in
+  let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic(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)) !res, Evd.universe_context evd
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
@@ -217,16 +226,23 @@ let stdlib_modules =
 
 let coq_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" stdlib_modules c)
+let coq_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" stdlib_modules c)
 
 let coq_mk_Setoid = coq_constant "Build_Setoid_Theory"
-let coq_cons = coq_constant "cons"
-let coq_nil = coq_constant "nil"
-let coq_None = coq_constant "None"
-let coq_Some = coq_constant "Some"
+let coq_None = coq_reference "None"
+let coq_Some = coq_reference "Some"
 let coq_eq = coq_constant "eq"
 
+let coq_cons = coq_reference "cons"
+let coq_nil = coq_reference "nil"
+
 let lapp f args = mkApp(Lazy.force f,args)
 
+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
   | App(f,args) when Array.length args >= 2 ->
@@ -255,17 +271,19 @@ let plugin_modules =
 
 let my_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
+let my_reference c =
+  lazy (Coqlib.gen_reference_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
-  make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"])
+  DirPath.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_ring_path) DirPath.empty (Label.make s))
 let znew_ring_path =
-  make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"])
+  DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s))
 
-let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
+let mk_cst l s = lazy (Coqlib.gen_reference "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 
 (* Ring theory *)
@@ -274,9 +292,9 @@ let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
 let coq_almost_ring_theory = my_constant "almost_ring_theory"
 
 (* setoid and morphism utilities *)
-let coq_eq_setoid = my_constant "Eqsth"
-let coq_eq_morph = my_constant "Eq_ext"
-let coq_eq_smorph = my_constant "Eq_s_ext"
+let coq_eq_setoid = my_reference "Eqsth"
+let coq_eq_morph = my_reference "Eq_ext"
+let coq_eq_smorph = my_reference "Eq_s_ext"
 
 (* ring -> almost_ring utilities *)
 let coq_ring_theory = my_constant "ring_theory"
@@ -303,16 +321,19 @@ let ltac_inv_morph_nothing = zltac"inv_morph_nothing"
 let coq_pow_N_pow_N = my_constant "pow_N_pow_N"
 
 (* hypothesis *)
-let coq_mkhypo = my_constant "mkhypo"
-let coq_hypo = my_constant "hypo"
+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
   interp_map
-    ((req,(function -1->Prot|_->Rec))::
+    ((global_head_of_constr req,(function -1->Prot|_->Rec))::
     List.map (fun (c,map) -> (Lazy.force c,map)) 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);
@@ -343,15 +364,12 @@ type ring_info =
       ring_pre_tac : glob_tactic_expr;
       ring_post_tac : glob_tactic_expr }
 
-module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
+module Cmap = Map.Make(Constr)
 
-let from_carrier = ref Cmap.empty
-let from_relation = ref Cmap.empty
-let from_name = ref Spmap.empty
+let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
+let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
 
 let ring_for_carrier r = Cmap.find r !from_carrier
-let ring_for_relation rel = Cmap.find rel !from_relation
-
 
 let find_ring_structure env sigma l =
   match l with
@@ -370,32 +388,9 @@ let find_ring_structure env sigma l =
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
-(*
-        let (req,_,_) = dest_rel cl in
-        (try ring_for_relation req
-        with Not_found ->
-          errorlabstrm "ring"
-            (str"cannot find a declared ring structure for equality"++
-             spc()++str"\""++pr_constr req++str"\"")) *)
-
-let _ =
-  Summary.declare_summary "tactic-new-ring-table"
-    { Summary.freeze_function =
-        (fun () -> !from_carrier,!from_relation,!from_name);
-      Summary.unfreeze_function =
-        (fun (ct,rt,nt) ->
-          from_carrier := ct; from_relation := rt; from_name := nt);
-      Summary.init_function =
-        (fun () ->
-          from_carrier := Cmap.empty; from_relation := Cmap.empty;
-          from_name := Spmap.empty) }
 
 let add_entry (sp,_kn) e =
-(*  let _ = ty e.ring_lemma1 in
-  let _ = ty e.ring_lemma2 in
-*)
   from_carrier := Cmap.add e.ring_carrier e !from_carrier;
-  from_relation := Cmap.add e.ring_req e !from_relation;
   from_name := Spmap.add sp e !from_name
 
 
@@ -408,10 +403,10 @@ let subst_th (subst,th) =
   let th' = subst_mps subst th.ring_th in
   let thm1' = subst_mps subst th.ring_lemma1 in
   let thm2' = subst_mps subst th.ring_lemma2 in
-  let tac'= subst_tactic subst th.ring_cst_tac in
-  let pow_tac'= subst_tactic subst th.ring_pow_tac in
-  let pretac'= subst_tactic subst th.ring_pre_tac in
-  let posttac'= subst_tactic subst th.ring_post_tac in
+  let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in
+  let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in
+  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 &&
@@ -443,20 +438,20 @@ let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
-      open_function = (fun i o -> if i=1 then cache_th o);
+      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x)}
 
 
-let setoid_of_relation env a r =
-  let evm = Evd.empty in
+let setoid_of_relation env evd a r =
   try
-    lapp coq_mk_Setoid
-      [|a ; r ;
-	Rewrite.get_reflexive_proof env evm a r ;
-	Rewrite.get_symmetric_proof env evm a r ;
-	Rewrite.get_transitive_proof env evm a r |]
+    let evm = !evd in
+    let evm, refl = Rewrite.get_reflexive_proof env evm a r in
+    let evm, sym = Rewrite.get_symmetric_proof env evm a r in
+    let evm, trans = Rewrite.get_transitive_proof env evm a r in
+      evd := evm;
+      lapp coq_mk_Setoid [|a ; r ; refl; sym; trans |]
   with Not_found ->
     error "cannot find setoid relation"
 
@@ -469,7 +464,7 @@ let op_smorph r add mul req m1 m2 =
 (* let default_ring_equality (r,add,mul,opp,req) = *)
 (*   let is_setoid = function *)
 (*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(*         eq_constr req rel (\* Qu: use conversion ? *\) *)
+(*         eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
 (*     | _ -> false in *)
 (*   match default_relation_for_carrier ~filter:is_setoid r with *)
 (*       Leibniz _ -> *)
@@ -484,7 +479,7 @@ let op_smorph r add mul req m1 m2 =
 (*         let is_endomorphism = function *)
 (*             { args=args } -> List.for_all *)
 (*                 (function (var,Relation rel) -> *)
-(*                   var=None && eq_constr req rel *)
+(*                   var=None && eq_constr_nounivs req rel *)
 (*                   | _ -> false) args in *)
 (*         let add_m = *)
 (*           try default_morphism ~filter:is_endomorphism add *)
@@ -519,17 +514,19 @@ let op_smorph r add mul req m1 m2 =
 (*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
 (*         (setoid,op_morph) *)
 
-let ring_equality (r,add,mul,opp,req) =
+let ring_equality env evd (r,add,mul,opp,req) =
   match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
-	let setoid = lapp coq_eq_setoid [|r|] in
+    | App (f, [| _ |]) when eq_constr_nounivs f (Lazy.force coq_eq) ->
+	let setoid = plapp evd coq_eq_setoid [|r|] in
 	let op_morph =
 	  match opp with
-              Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
-            | None -> lapp coq_eq_smorph [|r;add;mul|] in
+              Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
+            | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+	let setoid = Typing.solve_evars env evd setoid in
+	let op_morph = Typing.solve_evars env evd op_morph in
 	  (setoid,op_morph)
     | _ ->
-	let setoid = setoid_of_relation (Global.env ()) r req in
+	let setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
 	let add_m, add_m_lem =
 	  try Rewrite.default_morphism signature add
@@ -549,7 +546,7 @@ let ring_equality (r,add,mul,opp,req) =
 		let op_morph =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
-		    msgnl
+		    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++
@@ -558,7 +555,7 @@ let ring_equality (r,add,mul,opp,req) =
 		  op_morph)
             | None ->
 		(Flags.if_verbose
-		    msgnl
+		    msg_info
 		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
 			str"and morphisms \""++pr_constr add_m_lem ++
 			str"\""++spc()++str"and \""++
@@ -566,22 +563,22 @@ let ring_equality (r,add,mul,opp,req) =
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
-let build_setoid_params r add mul opp req eqth =
+let build_setoid_params env evd r add mul opp req eqth =
   match eqth with
       Some th -> th
-    | None -> ring_equality (r,add,mul,opp,req)
+    | None -> ring_equality env evd (r,add,mul,opp,req)
 
 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
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
-        when eq_constr f (Lazy.force coq_almost_ring_theory) ->
+        when eq_constr_nounivs 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 f (Lazy.force coq_semi_ring_theory) ->
+        when eq_constr_nounivs 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 f (Lazy.force coq_ring_theory) ->
+        when eq_constr_nounivs f (Lazy.force coq_ring_theory) ->
         (Some false,r,zero,one,add,mul,Some sub,Some opp,req)
     | _ -> error "bad ring structure"
 
@@ -591,18 +588,18 @@ let dest_morph env sigma m_spec =
   match kind_of_term m_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req;
               c;czero;cone;cadd;cmul;csub;copp;ceqb;phi|])
-        when eq_constr f (Lazy.force coq_ring_morph) ->
+        when eq_constr_nounivs f (Lazy.force coq_ring_morph) ->
           (c,czero,cone,cadd,cmul,Some csub,Some copp,ceqb,phi)
     | App(f,[|r;zero;one;add;mul;req;c;czero;cone;cadd;cmul;ceqb;phi|])
-        when eq_constr f (Lazy.force coq_semi_morph) ->
+        when eq_constr_nounivs f (Lazy.force coq_semi_morph) ->
         (c,czero,cone,cadd,cmul,None,None,ceqb,phi)
     | _ -> error "bad morphism structure"
 
 
-type coeff_spec =
-    Computational of constr (* equality test *)
+type 'constr coeff_spec =
+    Computational of 'constr (* equality test *)
   | Abstract (* coeffs = Z *)
-  | Morphism of constr (* general morphism *)
+  | Morphism of 'constr (* general morphism *)
 
 
 let reflect_coeff rkind =
@@ -618,101 +615,89 @@ type cst_tac_spec =
 
 let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
-      Some (CstTac t) -> Tacinterp.glob_tactic t
+      Some (CstTac t) -> Tacintern.glob_tactic t
     | Some (Closed lc) ->
         closed_term_ast (List.map Smartlocate.global_with_alias lc)
     | None ->
-        (match rk, opp, kind with
-            Abstract, None, _ ->
-              let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
-              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
-          | Abstract, Some opp, Some _ ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
-              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | Abstract, Some opp, None ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
-              TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
-          | Computational _,_,_ ->
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
-              TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
-          | Morphism mth,_,_ ->
-              let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
-              let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
-              TacArg
-                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
-
-let make_hyp env c =
-  let t = Retyping.get_type_of env Evd.empty c in
-  lapp coq_mkhypo [|t;c|]
-
-let make_hyp_list env lH =
-  let carrier = Lazy.force coq_hypo in
-  List.fold_right
-    (fun c l -> lapp coq_cons [|carrier; (make_hyp env c); l|]) lH
-    (lapp coq_nil [|carrier|])
-
-let interp_power env pow =
-  let carrier = Lazy.force coq_hypo in
+        let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
+              TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
+
+let make_hyp env evd c =
+  let t = Retyping.get_type_of env !evd c in
+   plapp evd coq_mkhypo [|t;c|]
+
+let make_hyp_list env evd lH =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+  let l = 
+    List.fold_right
+      (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
+      (plapp evd coq_nil [|carrier|])
+  in 
+  let l' = Typing.solve_evars env evd 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(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+      let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
+      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
-        | CstTac t -> Tacinterp.glob_tactic t
+        | CstTac t -> Tacintern.glob_tactic t
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
-      let spec = make_hyp env (ic spec) in
-      (tac, lapp coq_Some [|carrier; spec|])
+      let spec = make_hyp env evd (ic_unsafe spec) in
+      (tac, plapp evd coq_Some [|carrier; spec|])
 
-let interp_sign env sign =
-  let carrier = Lazy.force coq_hypo in
+let interp_sign env evd sign =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match sign with
-  | None -> lapp coq_None [|carrier|]
+  | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env (ic spec) in
-      lapp coq_Some [|carrier;spec|]
+      let spec = make_hyp env evd (ic_unsafe spec) in
+      plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let interp_div env div =
-  let carrier = Lazy.force coq_hypo in
+let interp_div env evd div =
+  let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match div with
-  | None -> lapp coq_None [|carrier|]
+  | None -> plapp evd coq_None [|carrier|]
   | Some spec ->
-      let spec = make_hyp env (ic spec) in
-      lapp coq_Some [|carrier;spec|]
+      let spec = make_hyp env evd (ic_unsafe spec) in
+      plapp evd coq_Some [|carrier;spec|]
        (* Same remark on ill-typed terms ... *)
 
-let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
+let add_theory name (sigma,rth) eqth morphth cst_tac (pre,post) power sign div =
   check_required_library (cdir@["Ring_base"]);
   let env = Global.env() in
-  let sigma = Evd.empty in
   let (kind,r,zero,one,add,mul,sub,opp,req) = dest_ring env sigma rth in
-  let (sth,ext) = build_setoid_params r add mul opp req eqth in
-  let (pow_tac, pspec) = interp_power env power in
-  let sspec = interp_sign env sign in
-  let dspec = interp_div env div in
+  let evd = ref sigma in
+  let (sth,ext) = build_setoid_params env evd r add mul opp req eqth 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 div in
   let rk = reflect_coeff morphth in
-  let params =
-    exec_tactic env 5 (zltac "ring_lemmas")
+  let params,ctx =
+    exec_tactic env !evd 5 (zltac "ring_lemmas")
       (List.map carg[sth;ext;rth;pspec;sspec;dspec;rk]) in
-  let lemma1 = constr_of params.(3) in
-  let lemma2 = constr_of params.(4) in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
 
-  let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
-  let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
+  let lemma1 =
+    decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in
+  let lemma2 =
+    decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let posttac =
     match post with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
@@ -720,9 +705,9 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
         { ring_carrier = r;
           ring_req = req;
           ring_setoid = sth;
-          ring_ext = constr_of params.(1);
-          ring_morph = constr_of params.(2);
-          ring_th = constr_of params.(0);
+          ring_ext = params.(1);
+          ring_morph = params.(2);
+          ring_th = params.(0);
           ring_cst_tac = cst_tac;
 	  ring_pow_tac = pow_tac;
           ring_lemma1 = lemma1;
@@ -731,22 +716,28 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
           ring_post_tac = posttac }) in
   ()
 
-type ring_mod =
-    Ring_kind of coeff_spec
+type 'constr ring_mod =
+    Ring_kind of 'constr coeff_spec
   | Const_tac of cst_tac_spec
   | Pre_tac of raw_tactic_expr
   | Post_tac of raw_tactic_expr
-  | Setoid of Topconstr.constr_expr * Topconstr.constr_expr
-  | Pow_spec of cst_tac_spec * Topconstr.constr_expr
+  | Setoid of Constrexpr.constr_expr * Constrexpr.constr_expr
+  | Pow_spec of cst_tac_spec * Constrexpr.constr_expr
            (* Syntaxification tactic , correctness lemma *)
-  | Sign_spec of Topconstr.constr_expr
-  | Div_spec of Topconstr.constr_expr
+  | Sign_spec of Constrexpr.constr_expr
+  | Div_spec of Constrexpr.constr_expr
+
+
+let ic_coeff_spec = function
+  | Computational t -> Computational (ic_unsafe t)
+  | Morphism t -> Morphism (ic_unsafe t)
+  | Abstract -> Abstract
 
 
 VERNAC ARGUMENT EXTEND ring_mod
-  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational (ic eq_test)) ]
+  | [ "decidable" constr(eq_test) ] -> [ Ring_kind(Computational eq_test) ]
   | [ "abstract" ] -> [ Ring_kind Abstract ]
-  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism (ic morph)) ]
+  | [ "morphism" constr(morph) ] -> [ Ring_kind(Morphism morph) ]
   | [ "constants" "[" tactic(cst_tac) "]" ] -> [ Const_tac(CstTac cst_tac) ]
   | [ "closed" "[" ne_global_list(l) "]" ] -> [ Const_tac(Closed l) ]
   | [ "preprocess" "[" tactic(pre) "]" ] -> [ Pre_tac pre ]
@@ -761,7 +752,7 @@ VERNAC ARGUMENT EXTEND ring_mod
 END
 
 let set_once s r v =
-  if !r = None then r := Some v else error (s^" cannot be set twice")
+  if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
 
 let process_ring_mods l =
   let kind = ref None in
@@ -773,21 +764,29 @@ let process_ring_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_kind k -> set_once "ring kind" kind k
+      Ring_kind k -> set_once "ring kind" kind (ic_coeff_spec k)
     | Const_tac t -> set_once "tactic recognizing constants" cst_tac t
     | Pre_tac t -> set_once "preprocess tactic" pre t
     | Post_tac t -> set_once "postprocess tactic" post t
-    | Setoid(sth,ext) -> set_once "setoid" set (ic sth,ic ext)
+    | Setoid(sth,ext) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
     | Pow_spec(t,spec) -> set_once "power" power (t,spec)
     | Sign_spec t -> set_once "sign" sign t
     | Div_spec t -> set_once "div" div t) l;
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidRing
+VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods(l) ] ->
     [ 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]
+  | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
+    msg_notice (strbrk "The following ring structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.ring_req))
+    ) !from_name ]
 END
 
 (*****************************************************************************)
@@ -799,10 +798,11 @@ let make_args_list rl t =
   | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2]
   | _ -> rl
 
-let make_term_list carrier rl =
-  List.fold_right
-    (fun x l -> lapp coq_cons [|carrier;x;l|]) rl
-    (lapp coq_nil [|carrier|])
+let make_term_list env evd carrier rl =
+  let l = List.fold_right
+    (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
+    (plapp evd coq_nil [|carrier|])
+  in Typing.solve_evars env evd l
 
 let ltac_ring_structure e =
   let req = carg e.ring_req in
@@ -819,19 +819,24 @@ let ltac_ring_structure e =
   [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 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
+let ring_lookup (f:glob_tactic_expr) lH rl t =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try (* find_ring_strucure can raise an exception *)
+      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 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
 
 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
 
 
@@ -839,10 +844,10 @@ END
 (***********************************************************************)
 
 let new_field_path =
-  make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"])
+  DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s))
 
 
 let _ = add_map "field"
@@ -851,9 +856,9 @@ let _ = add_map "field"
     coq_nil, (function -1->Eval|_ -> Prot);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
-    my_constant "display_linear",
+    my_reference "display_linear",
       (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
-    my_constant "display_pow_linear",
+    my_reference "display_pow_linear",
      (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
@@ -865,16 +870,16 @@ let _ = add_map "field"
     pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
     (* FEeval: evaluate morphism, protect field
        operations and make recursive call on the var map *)
-    my_constant "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
-  (map_with_eq
+  (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
        operations and make recursive call on the var map *)
-     my_constant "PCond", (function -1|8|10|13->Eval|12->Rec|_->Prot)]);;
-(*                       (function -1|8|10->Eval|9->Rec|_->Prot)]);;*)
+     my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
+(*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
 
 
 let _ = Redexpr.declare_reduction "simpl_field_expr"
@@ -882,29 +887,29 @@ let _ = Redexpr.declare_reduction "simpl_field_expr"
 
 
 
-let afield_theory = my_constant "almost_field_theory"
-let field_theory = my_constant "field_theory"
-let sfield_theory = my_constant "semi_field_theory"
-let af_ar = my_constant"AF_AR"
-let f_r = my_constant"F_R"
-let sf_sr = my_constant"SF_SR"
-let dest_field env sigma th_spec =
-  let th_typ = Retyping.get_type_of env sigma th_spec in
+let afield_theory = my_reference "almost_field_theory"
+let field_theory = my_reference "field_theory"
+let sfield_theory = my_reference "semi_field_theory"
+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 th_typ = Retyping.get_type_of env !evd th_spec in
   match kind_of_term th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
-        when eq_constr f (Lazy.force afield_theory) ->
-        let rth = lapp af_ar
+        when is_global (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 eq_constr f (Lazy.force field_theory) ->
+        when is_global (Lazy.force field_theory) f ->
         let rth =
-          lapp f_r
+          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 eq_constr f (Lazy.force sfield_theory) ->
-        let rth = lapp sf_sr
+        when is_global (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)
     | _ -> error "bad field structure"
@@ -922,13 +927,10 @@ type field_info =
       field_pre_tac : glob_tactic_expr;
       field_post_tac : glob_tactic_expr }
 
-let field_from_carrier = ref Cmap.empty
-let field_from_relation = ref Cmap.empty
-let field_from_name = ref Spmap.empty
-
+let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
+let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
 let field_for_carrier r = Cmap.find r !field_from_carrier
-let field_for_relation rel = Cmap.find rel !field_from_relation
 
 let find_field_structure env sigma l =
   check_required_library (cdir@["Field_tac"]);
@@ -948,35 +950,9 @@ let find_field_structure env sigma l =
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
-(*        let (req,_,_) = dest_rel cl in
-        (try field_for_relation req
-        with Not_found ->
-          errorlabstrm "field"
-            (str"cannot find a declared field structure for equality"++
-             spc()++str"\""++pr_constr req++str"\"")) *)
-
-let _ =
-  Summary.declare_summary "tactic-new-field-table"
-    { Summary.freeze_function =
-        (fun () -> !field_from_carrier,!field_from_relation,!field_from_name);
-      Summary.unfreeze_function =
-        (fun (ct,rt,nt) ->
-          field_from_carrier := ct; field_from_relation := rt;
-          field_from_name := nt);
-      Summary.init_function =
-        (fun () ->
-          field_from_carrier := Cmap.empty; field_from_relation := Cmap.empty;
-          field_from_name := Spmap.empty) }
 
 let add_field_entry (sp,_kn) e =
-(*
-  let _ = ty e.field_ok in
-  let _ = ty e.field_simpl_eq_ok in
-  let _ = ty e.field_simpl_ok in
-  let _ = ty e.field_cond in
-*)
   field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier;
-  field_from_relation := Cmap.add e.field_req e !field_from_relation;
   field_from_name := Spmap.add sp e !field_from_name
 
 let subst_th (subst,th) =
@@ -987,10 +963,10 @@ let subst_th (subst,th) =
   let thm3' = subst_mps subst th.field_simpl_ok in
   let thm4' = subst_mps subst th.field_simpl_eq_in_ok in
   let thm5' = subst_mps subst th.field_cond in
-  let tac'= subst_tactic subst th.field_cst_tac in
-  let pow_tac' = subst_tactic subst th.field_pow_tac in
-  let pretac'= subst_tactic subst th.field_pre_tac in
-  let posttac'= subst_tactic subst th.field_post_tac in
+  let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in
+  let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in
   if c' == th.field_carrier &&
      eq' == th.field_req &&
      thm1' == th.field_ok &&
@@ -1019,17 +995,17 @@ let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
-      open_function = (fun i o -> if i=1 then cache_th o);
+      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x) }
 
-let field_equality r inv req =
+let field_equality evd r inv req =
   match kind_of_term req with
-    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
-        mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
+    | 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|])
     | _ ->
-	let _setoid = setoid_of_relation (Global.env ()) r req in
+	let _setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req)],Some(r,Some req) in
 	let inv_m, inv_m_lem =
 	  try Rewrite.default_morphism signature inv
@@ -1037,45 +1013,50 @@ let field_equality r inv req =
             error "field inverse should be declared as a morphism" in
 	  inv_m_lem
 
-let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
+let add_field_theory name (sigma,fth) eqth morphth cst_tac inj (pre,post) power sign odiv =
   check_required_library (cdir@["Field_tac"]);
   let env = Global.env() in
-  let sigma = Evd.empty in
+  let evd = ref sigma in
   let (kind,r,zero,one,add,mul,sub,opp,div,inv,req,rth) =
-    dest_field env sigma fth in
-  let (sth,ext) = build_setoid_params r add mul opp req eqth in
+    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 rth eqth morphth cst_tac (None,None) power sign odiv in
-  let (pow_tac, pspec) = interp_power env power in
-  let sspec = interp_sign env sign in
-  let dspec = interp_div env odiv in
-  let inv_m = field_equality r inv req in
+  let _ = add_theory 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
+  let inv_m = field_equality evd r inv req in
   let rk = reflect_coeff morphth in
-  let params =
-    exec_tactic env 9 (field_ltac"field_lemmas")
+  let params,ctx =
+    exec_tactic env !evd 9 (field_ltac"field_lemmas")
       (List.map carg[sth;ext;inv_m;fth;pspec;sspec;dspec;rk]) in
-  let lemma1 = constr_of params.(3) in
-  let lemma2 = constr_of params.(4) in
-  let lemma3 = constr_of params.(5) in
-  let lemma4 = constr_of params.(6) in
+  let lemma1 = params.(3) in
+  let lemma2 = params.(4) in
+  let lemma3 = params.(5) in
+  let lemma4 = params.(6) in
   let cond_lemma =
     match inj with
-      | Some thm -> mkApp(constr_of params.(8),[|thm|])
-      | None -> constr_of params.(7) in
-  let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in
-  let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in
-  let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
-  let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in
-  let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in
+      | Some thm -> mkApp(params.(8),[|thm|])
+      | None -> params.(7) in
+  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
+    ctx lemma1 in
+  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") 
+    ctx lemma2 in
+  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") 
+    ctx lemma3 in
+  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") 
+    ctx lemma4 in
+  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") 
+    ctx cond_lemma in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let posttac =
     match post with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
@@ -1092,9 +1073,9 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
           field_pre_tac = pretac;
           field_post_tac = posttac }) in  ()
 
-type field_mod =
-    Ring_mod of ring_mod
-  | Inject of Topconstr.constr_expr
+type 'constr field_mod =
+    Ring_mod of 'constr ring_mod
+  | Inject of Constrexpr.constr_expr
 
 VERNAC ARGUMENT EXTEND field_mod
   | [ ring_mod(m) ] -> [ Ring_mod m ]
@@ -1112,23 +1093,31 @@ let process_field_mods l =
   let power = ref None in
   let div = ref None in
   List.iter(function
-      Ring_mod(Ring_kind k) -> set_once "field kind" kind k
+      Ring_mod(Ring_kind k) -> set_once "field kind" kind (ic_coeff_spec k)
     | Ring_mod(Const_tac t) ->
         set_once "tactic recognizing constants" cst_tac t
     | Ring_mod(Pre_tac t) -> set_once "preprocess tactic" pre t
     | Ring_mod(Post_tac t) -> set_once "postprocess tactic" post t
-    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic sth,ic ext)
+    | Ring_mod(Setoid(sth,ext)) -> set_once "setoid" set (ic_unsafe sth,ic_unsafe ext)
     | Ring_mod(Pow_spec(t,spec)) -> set_once "power" power (t,spec)
     | Ring_mod(Sign_spec t) -> set_once "sign" sign t
     | Ring_mod(Div_spec t) -> set_once "div" div t
-    | Inject i -> set_once "infinite property" inj (ic i)) l;
+    | Inject i -> set_once "infinite property" inj (ic_unsafe i)) l;
   let k = match !kind with Some k -> k | None -> Abstract in
   (k, !set, !inj, !cst_tac, !pre, !post, !power, !sign, !div)
 
-VERNAC COMMAND EXTEND AddSetoidField
+VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods(l) ] ->
   [ 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]
+| [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
+    msg_notice (strbrk "The following field structures have been declared:");
+    Spmap.iter (fun fn fi ->
+      msg_notice (hov 2
+        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+          str"with carrier "++ pr_constr fi.field_carrier++spc()++
+          str"and equivalence relation "++ pr_constr fi.field_req))
+    ) !field_from_name ]
 END
 
 
@@ -1146,18 +1135,23 @@ let ltac_field_structure e =
   [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 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
+let field_lookup (f:glob_tactic_expr) lH rl t =
+  Proofview.Goal.enter begin fun gl ->
+    let sigma = Proofview.Goal.sigma gl in
+    let env = Proofview.Goal.env gl in
+    try
+      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 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
 
 
 TACTIC EXTEND field_lookup
 | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] ->
-      [ let (t,l) = list_sep_last lt in field_lookup f lH l t ]
+      [ let (t,l) = List.sep_last lt in field_lookup f lH l t ]
 END