aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-10-30 11:03:26 +0100
committerMaxime Dénès2018-10-30 13:10:02 +0100
commit6214079b980b8a02bef20d5b25abbe49c3095f32 (patch)
tree7f50070252445fa2147f81c7d0aeb65158e1ac0d /kernel/nativelambda.ml
parent0ac673e562c34245e4e48efc428d808e917be79b (diff)
Distinguish globalization and pretyping error on unbound variable
We can then avoid passing an empty env.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions