Merge PR #6935: Separate universe minimization and evar normalization functions

3 files changed, 10 insertions, 12 deletions

diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 845104c3c..e331dc014 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -563,8 +563,8 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
   (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. 
 If someone knows how to prevent solved existantial removal in  understand, please do not hesitate to change the computation of [ctx] here *) 
   let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
-  let ctx, f = Evarutil.nf_evars_and_universes ctx in
-  let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in
+  let ctx = Evd.minimize_universes ctx in
+  let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in
 
   (* then we map [rt] to replace the implicit holes by their values *)
   let rec change rt =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index fb9ae64bf..e41bf71dd 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1533,14 +1533,12 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let env = Global.env() in
   let evd = Evd.from_env env in
   let evd, function_type = interp_type_evars env evd type_of_f in
-  let function_type = EConstr.Unsafe.to_constr function_type in
-  let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
+  let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
-  let ty = EConstr.Unsafe.to_constr ty in
-  let evd, nf = Evarutil.nf_evars_and_universes evd in
-  let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in
-  let function_type = nf function_type in
+  let evd = Evd.minimize_universes evd in
+  let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in
+  let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
   let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 99bb8440c..33c30e4d3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -186,8 +186,8 @@ let dummy_goal env sigma =
     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 -> EConstr.Unsafe.to_constr c
+let constr_of evd v = match Value.to_constr v with
+  | Some c -> EConstr.to_constr evd c
   | None -> failwith "Ring.exec_tactic: anomaly"
 
 let tactic_res = ref [||]
@@ -221,8 +221,8 @@ let exec_tactic env evd n f args =
   (** 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
-  let nf c = nf (constr_of c) in
+  let evd = Evd.minimize_universes (Refiner.project gls) in
+  let nf c = constr_of evd c in
   Array.map nf !tactic_res, Evd.universe_context_set evd
 
 let stdlib_modules =