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/record.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/record.ml')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index d85b71df44..5be911938b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records = in let univs = Evd.check_univ_decl ~poly sigma decl in let ubinders = Evd.universe_binders sigma in - let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in + let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in let () = List.iter (iter_constr ce) (List.rev newps) in ubinders, univs, template, newps, imps, ans |