diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-03-04 18:17:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-03-04 18:17:56 +0100 |
| commit | 120053a50f87bd53398eedc887fa5e979f56f112 (patch) | |
| tree | 06f3bd294439a2cd62512b41a599f2c7b277cba6 /library | |
| parent | b98e4857a13a4014c65882af5321ebdb09f41890 (diff) | |
This fix is probably not enough to justify that there are no problems with
primitive projections and prop. ext. or univalence, but at least it prevents
known proofs of false (see discussion on #4588).
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions