diff options
Diffstat (limited to 'toplevel/classes.ml')
| -rw-r--r-- | toplevel/classes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 0a83c49c8d..2fc0f5ff19 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -191,7 +191,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in nf t in - Evarutil.check_evars env Evd.empty !evars termtype; + Pretyping.check_evars env Evd.empty !evars termtype; let pl, ctx = Evd.universe_context ?names:pl !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry @@ -287,7 +287,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro let evm, nf = Evarutil.nf_evar_map_universes !evars in let termtype = nf termtype in let _ = (* Check that the type is free of evars now. *) - Evarutil.check_evars env Evd.empty evm termtype + Pretyping.check_evars env Evd.empty evm termtype in let term = Option.map nf term in if not (Evd.has_undefined evm) && not (Option.is_empty term) then @@ -330,7 +330,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) }; + Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) }; Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] @@ -361,7 +361,7 @@ let context poly l = let _, ((env', fullctx), impls) = interp_context_evars env evars l in let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in let fullctx = Context.Rel.map subst fullctx in - let ce t = Evarutil.check_evars env Evd.empty !evars t in + let ce t = Pretyping.check_evars env Evd.empty !evars t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = try named_of_rel_context fullctx |