diff options
| author | Gaëtan Gilbert | 2020-01-29 16:36:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-29 16:52:19 +0100 |
| commit | f86fd4b52a29e2ef63f03cc67c845f1fa05aae13 (patch) | |
| tree | 8eed7cda2bb37ac825474e19c1048d1d68d24b5a /kernel/nativecode.ml | |
| parent | 8c04d108e1f57d0e8e11483a7c9de721ab2f026a (diff) | |
Nicer kernel universe error for inductives
Not sure if it's possible to see it without a plugin.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions