aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-10-21 11:56:37 +0200
committerPierre-Marie Pédrot2015-10-21 11:56:37 +0200
commitde2031b8fa2a7e236d734500294ebd5050fcb7d5 (patch)
tree45dbc53e791751456e7ba153135b7f7f01451849 /kernel/nativelambda.mli
parent2d747797c427818cdf85d0a0d701c7c9b0106b82 (diff)
Removing test for bug #3956.
It breaks test-suite of trunk since Matthieu's fixes for the soundness of polymorphic universes, and I am unsure of the expected semantics. We should reintroduce it later on when we understand better the issue of simply fix it once and for all.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions