diff options
| author | Gaëtan Gilbert | 2019-10-29 13:20:04 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-12-16 11:48:53 +0100 |
| commit | 62adf2b9e03afa212fcd8819226da068bf4a32b8 (patch) | |
| tree | f21b6feeec930f418c0a3302fb9c50bfc13c384d /vernac/comAssumption.ml | |
| parent | 1df9e71a1f9b0729a17d09e009add2e87fcde5ad (diff) | |
Pretyping.check_evars: make initial evar map optional
There are no users in Coq but maybe some plugin wants it so don't
completely remove it
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 -> |