diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a001420f74..8a403e5a03 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -255,7 +255,7 @@ let context ~poly l = let sigma, (_, ((_env, ctx), impls)) = interp_context_evars ~program_mode:false 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.from_env env) sigma t in + let ce t = Pretyping.check_evars env sigma t in let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in (* reorder, evar-normalize and add implicit status *) let ctx = List.rev_map (fun d -> |