diff options
| author | Matthieu Sozeau | 2014-08-03 23:19:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-03 23:39:02 +0200 |
| commit | ead5d80dff08f97998e81acfb2562dde741a26af (patch) | |
| tree | 7b5ad21993d0c1625f6609eba0e385378ca43faf /proofs/proof_errors.ml | |
| parent | ef72be87579be34e9454fe1f785ff36a9c25246c (diff) | |
Fix infer conv using the wrong universe conversion flexibility information
for constants that are not unfolded during conversion.
Fix discharge of polymorphic section variables over inductive types.
Diffstat (limited to 'proofs/proof_errors.ml')
0 files changed, 0 insertions, 0 deletions