diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-13 16:11:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-13 17:40:27 +0200 |
| commit | df6e64fd28e9ba8b12045768869c7f083a15e9c0 (patch) | |
| tree | 710352f7afc09981336c5da43da1fa6c10628435 /coq-win32.itarget | |
| parent | f49137b917fa7561eb53a87155ed57b3dbc70d90 (diff) | |
Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of an anomaly in case
a universe inconsistency occurs when applying a coercion. The statement of the test-suite file
cannot check as is, but does check when the correct FunctorCategory is given, instantiating the TypeCat
to Set.
Diffstat (limited to 'coq-win32.itarget')
0 files changed, 0 insertions, 0 deletions