diff options
| author | Pierre-Marie Pédrot | 2015-10-21 11:56:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-21 11:56:37 +0200 |
| commit | de2031b8fa2a7e236d734500294ebd5050fcb7d5 (patch) | |
| tree | 45dbc53e791751456e7ba153135b7f7f01451849 /kernel/nativecode.mli | |
| parent | 2d747797c427818cdf85d0a0d701c7c9b0106b82 (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/nativecode.mli')
0 files changed, 0 insertions, 0 deletions