diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-03 17:44:34 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 14:55:49 +0200 |
| commit | dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 (patch) | |
| tree | 33fdd7c2eb44e54e7777e2d074127b129c5385ac /vernac/classes.ml | |
| parent | d2533da244f770261478ae829167cb3a8ad38038 (diff) | |
Remove some occurrences of Evd.empty
We address the easy ones, but they should probably be all removed.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 61ce5d6c4..d99d45313 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -196,7 +196,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in let sigma = Evd.minimize_universes sigma in - Pretyping.check_evars env Evd.empty sigma termtype; + Pretyping.check_evars env (Evd.from_env env) sigma termtype; let univs = Evd.check_univ_decl ~poly sigma decl in let termtype = to_constr sigma termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id @@ -290,7 +290,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (* Beware of this step, it is required as to minimize universes. *) let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) - Pretyping.check_evars env Evd.empty sigma termtype; + Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in if not (Evd.has_undefined sigma) && not (Option.is_empty term) then @@ -365,7 +365,7 @@ let context poly l = let sigma, (_, ((env', fullctx), impls)) = interp_context_evars env sigma l in (* Note, we must use the normalized evar from now on! *) let sigma = Evd.minimize_universes sigma in - let ce t = Pretyping.check_evars env Evd.empty sigma t in + let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in let ctx = try named_of_rel_context fullctx |