Deprecate mixing univ minimization and evm normalization functions.

Normalization sounds like it should be semantically noop.

1 files changed, 4 insertions, 6 deletions

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