diff options
| author | msozeau | 2009-11-06 22:41:38 +0000 |
|---|---|---|
| committer | msozeau | 2009-11-06 22:41:38 +0000 |
| commit | 6d684ec32bc62ff1e9528081a2369852cc5b5c65 (patch) | |
| tree | 9a972ff099f0ad26296cb0802008cda401dc8ee7 /interp/implicit_quantifiers.ml | |
| parent | 4237fa16d23101bc05ebc9a3dad168be4f3f64d8 (diff) | |
- Fix discharge bug in typeclasses: some constrs were not actually
discharged on the other definitions in the section.
- Avoid universe problem in generalize_eqs were we could give an
[@eq_refl Set x x] proof where an [@eq Type x x] was expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions