aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGaëtan Gilbert2017-11-10 13:23:32 +0100
committerGaëtan Gilbert2018-02-10 01:34:19 +0100
commit1ed0836a7e0c8e05b0288f85e344ef5249d5d228 (patch)
treee36199b1ff1f6a7ddf83ba164c131339b5061f6c /kernel
parent35fba70509d9fb219b2a88f8e7bd246b2671b39b (diff)
Inference of inductive subtyping does not need an evar map.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions