diff options
| author | herbelin | 2009-09-27 09:33:17 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-27 09:33:17 +0000 |
| commit | 030bb74f41697f58126a1358408150bd75f35be1 (patch) | |
| tree | 845dec2d0823d38991ac599d2b33e250cfecc17d /doc/stdlib/Library.tex | |
| parent | e2bc6bdd5d40e80e941ef83048e3b6aa92ad1cee (diff) | |
Apply "Declare Implicit Tactic" also to terms interpreted as "open
terms". Let's hope the different instantiation mechanisms (implicit
tactic, type classes, information coming from the with clause, ...)
will combine not to badly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12361 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/stdlib/Library.tex')
0 files changed, 0 insertions, 0 deletions