diff options
| author | Hugo Herbelin | 2015-10-22 22:25:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-22 22:37:44 +0200 |
| commit | 273005ac85e9ae0c23328e243edeadfc8dcaf8bb (patch) | |
| tree | 4084d81a08d34d541122fb3fc91574bce1003ba5 /kernel/nativecode.ml | |
| parent | 95b04506542064fbda7a61c4b6ce276a668d25bd (diff) | |
Fixing a bug in reporting ill-formed inductive.
Was introduced in b06d3badb (15 Jul 2015).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions