diff options
| author | msozeau | 2008-10-22 16:25:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-10-22 16:25:12 +0000 |
| commit | 6322f01644dd370322b09b663c53eef57388dcce (patch) | |
| tree | c498df27a9dbd282169adced997b25021400ca7c /doc/stdlib/Library.tex | |
| parent | e03d1840a8e6eec927e7fbe006d59ab21b8d818f (diff) | |
A much better implementation of implicit generalization:
- Do it after internalisation (esp. after notation expansion)
- Generalize it to any constr, not just typeclasses
- Prepare for having settings on the implicit status of generalized
variables (currently only impl,impl and expl,expl are supported).
- Simplified implementation! (Still some refactoring needed in
typeclasses parsing code).
This patch contains a fix for bug #1964 as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib/Library.tex')
0 files changed, 0 insertions, 0 deletions