Commit 2019-10-01 18:48 5ed5f594
View on Github →feat(tactic/delta_instance): handle parameters and use in library (#1483)
- feat(tactic/core): improve delta_instance handler
- feat(*): use delta_instance derive handler
- feat(tactic/delta_instance): cleaner handling of application under binders
- Revert "feat(tactic/delta_instance): cleaner handling of application under binders" This reverts commit 4005a2fad571bf922c98f94cbc1154666abc259d.
- comment apply_under_pis
- properly get unused name
- feat(tactic/delta_instance): run with high priority and don't run on inductives
- Update src/tactic/core.lean Co-Authored-By: Floris van Doorn fpvdoorn@gmail.com