aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comFixpoint.ml2
-rw-r--r--vernac/comInductive.ml10
-rw-r--r--vernac/lemmas.ml2
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml9
6 files changed, 16 insertions, 15 deletions
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