Deprecate mixing univ minimization and evm normalization functions.

Normalization sounds like it should be semantically noop.

12 files changed, 33 insertions, 31 deletions

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 40c1ee082..8bb0d2f61 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -178,11 +178,14 @@ val nf_evar_map_undefined : evar_map -> evar_map
 val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
 
 val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
 val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
 
 (** Normalize the evar map w.r.t. universes, after simplification of constraints.
     Return the substitution function for constrs as well. *)
 val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"]
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of Evar.t
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 =
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 6bd4866c6..70f73df5c 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
 	mib.mind_nparams in
     let sigma, sort = Evd.fresh_sort_in_family env sigma sort in
     let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
-    let sigma, nf = Evarutil.nf_evars_and_universes sigma in
-      (nf c', Evd.evar_universe_context sigma), eff
+    let sigma = Evd.minimize_universes sigma in
+    (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff
   else
     let sigma, pind = Evd.fresh_inductive_instance env sigma ind in
     let sigma, c = build_induction_scheme env sigma pind dep sort in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aae4bc088..482571ea8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4929,9 +4929,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
 
   let evd, ctx, concl =
     (* FIXME: should be done only if the tactic succeeds *)
-    let evd, nf = nf_evars_and_universes !evdref in
+    let evd = Evd.minimize_universes !evdref in
     let ctx = Evd.universe_context_set evd in
-      evd, ctx, nf concl
+      evd, ctx, Evarutil.nf_evars_universes evd concl
   in
   let concl = EConstr.of_constr concl in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3c133f317..a98fc15ce 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -196,7 +196,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	in
 	let (_, ty_constr) = instance_constructor (k,u) subst in
         let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-        let sigma,_ = Evarutil.nf_evars_and_universes sigma in
+        let sigma = Evd.minimize_universes sigma in
         Pretyping.check_evars env Evd.empty sigma termtype;
         let univs = Evd.check_univ_decl ~poly sigma decl in
         let termtype = to_constr sigma termtype in
@@ -289,7 +289,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
       let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:false env sigma in
       let sigma = Evarutil.nf_evar_map_undefined sigma in
       (* Beware of this step, it is required as to minimize universes. *)
-      let sigma, _nf = Evarutil.nf_evar_map_universes sigma in
+      let sigma = Evd.minimize_universes sigma in
       (* Check that the type is free of evars now. *)
       Pretyping.check_evars env Evd.empty sigma termtype;
       let termtype = to_constr sigma termtype in
@@ -365,7 +365,7 @@ let context poly l =
   let sigma = Evd.from_env env in
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in
   (* Note, we must use the normalized evar from now on! *)
-  let sigma,_ = Evarutil.nf_evars_and_universes sigma in
+  let sigma = Evd.minimize_universes sigma in
   let ce t = Pretyping.check_evars env Evd.empty sigma t in
   let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
   let ctx =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1466fa243..7b382dacc 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -224,7 +224,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
 
   (* Instantiate evars and check all are resolved *)
   let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
-  let sigma, _ = nf_evars_and_universes sigma in
+  let sigma = Evd.minimize_universes sigma in
   (* XXX: We still have evars here in Program *)
   let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
   let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 05c40dbdd..101298ef4 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -304,14 +304,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   (* Try further to solve evars, and instantiate them *)
   let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in
   (* Compute renewed arities *)
-  let sigma, nf = nf_evars_and_universes sigma in
+  let sigma = Evd.minimize_universes sigma in
+  let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
   let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
   let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
-  let sigma, nf' = nf_evars_and_universes sigma in
-  let arities = List.map nf' arities in
-  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
+  let sigma = Evd.minimize_universes sigma in
+  let nf = Evarutil.nf_evars_universes sigma in
+  let arities = List.map nf arities in
+  let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
   let uctx = Evd.check_univ_decl ~poly sigma decl in
   List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 30dd6ec74..aba5e32db 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
            (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
       evd thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
-  let evd, _nf = Evarutil.nf_evars_and_universes evd in
+  let evd = Evd.minimize_universes evd in
   (* XXX: This nf_evar is critical too!! We are normalizing twice if
      you look at the previous lines... *)
   let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
diff --git a/vernac/record.ml b/vernac/record.ml
index 78e68e8a3..b89c0060d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -168,7 +168,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
           EConstr.mkSort (Sorts.sort_of_univ univ)
         else sigma, typ
   in
-  let sigma, _ = Evarutil.nf_evars_and_universes sigma in
+  let sigma = Evd.minimize_universes sigma in
   let newfs = List.map (EConstr.to_rel_decl sigma) newfs in
   let newps = List.map (EConstr.to_rel_decl sigma) newps in
   let typ = EConstr.to_constr sigma typ in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a9d1631ba..b9600d23d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1619,17 +1619,16 @@ let vernac_check_may_eval ~atts redexp glopt rc =
   let glopt = query_command_selector ?loc:atts.loc glopt in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr env sigma rc in
-  let c = EConstr.Unsafe.to_constr c in
   let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
   Evarconv.check_problems_are_solved env sigma';
-  let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
+  let sigma' = Evd.minimize_universes sigma' in
   let uctx = Evd.universe_context_set sigma' in
   let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
-  let c = nf c in
   let j =
-    if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
-      Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c))
+    if Evarutil.has_undefined_evars sigma' c then
+      Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c)
     else
+      let c = EConstr.to_constr sigma' c in
       (* OK to call kernel which does not support evars *)
       Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
   in