diff options
| author | Hugo Herbelin | 2015-07-27 11:03:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-27 14:20:44 +0200 |
| commit | 9b690c608c2a48b26a8ac94325fe0008d438fb3b (patch) | |
| tree | f4d1c6619cd5d2687b2213dbfc340fec1119f3e7 /kernel/nativecode.ml | |
| parent | cb6c3ec2e66e3019cb9ee881b1e222e6e3691463 (diff) | |
Improving over 26aa224293 in reporting unexpected error during scheme creation.
This should actually probably be an anomaly, but I'm unsure the code
for decidability schemes is robust enough to dare it.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions