diff options
| author | msozeau | 2009-12-19 17:58:53 +0000 |
|---|---|---|
| committer | msozeau | 2009-12-19 17:58:53 +0000 |
| commit | fc3b7b356e68dba0bbabd8bf755c3a836f6a6396 (patch) | |
| tree | 6d5b343339c7675924311f1d54a6814d31a16923 /dev | |
| parent | 3319ae45b302f17c76dd19ff95c9785d9ba04557 (diff) | |
Backtrack on making exact hints for lemmas starting with products
(e.g. transitivity lemmas) and fix bug #2207, avoiding the generation of
useless eta-redexes during type class instance resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12600 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions