aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-10-19 18:13:32 +0200
committerMatthieu Sozeau2015-10-19 18:33:20 +0200
commit7d6d9c5aea6232200b99e828b7e04b49808f8478 (patch)
tree18951951e8f92b58e34ac650803c6c86e428aff7 /kernel/nativecode.mli
parent50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (diff)
Do occur-check w.r.t existential's types also when instantiating an evar.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions