diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-04-07 12:53:41 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
commit | 105db906ae45e792d1caeeb2e3fb7f69944b2caa (patch) | |
tree | b12ca28e6b172d2524c6a11c851c7d568f6a2411 /theories/Program | |
parent | b17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (diff) |
- Fixes for canonical structure resolution (check that the initial term indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
Diffstat (limited to 'theories/Program')
0 files changed, 0 insertions, 0 deletions