diff options
| author | Matthieu Sozeau | 2015-12-04 15:14:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-12-04 15:14:23 +0100 |
| commit | 9ee4a02e9234ad6cebb3365881250d7539d00d03 (patch) | |
| tree | fc917c980e80944343d81851a9666117c35d15fa /dev/include | |
| parent | f41968d8c240db4653d0b9fe76e1646cd7c6fb68 (diff) | |
Fix in setoid_rewrite in Type: avoid the generation of a rigid universe
on applications of inverse (flip) on a crelation.
This was poluting universe constraints of lemmas using generalized
rewriting in Type.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions