Improvements in typeclasses eauto and generalized rewriting:

- Decorate proof search with depth/subgoal number information
- Add a tactic [autoapply foo using hints] to call the resolution tactic
with the [transparent_state] associated with a hint db, giving better
control over unfolding.
- Fix a bug in the Lambda case in the new rewrite
- More work on the [Proper] and [subrelation] hints to cut the search space
while retaining completeness.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12118 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions