aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-10-29 13:20:04 +0100
committerGaëtan Gilbert2019-12-16 11:48:53 +0100
commit62adf2b9e03afa212fcd8819226da068bf4a32b8 (patch)
treef21b6feeec930f418c0a3302fb9c50bfc13c384d /kernel
parent1df9e71a1f9b0729a17d09e009add2e87fcde5ad (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 'kernel')
0 files changed, 0 insertions, 0 deletions