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

6 files changed, 16 insertions, 15 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 7f2642093..2e1bd6970 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 8c48490ff..564c0965b 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