Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore(tactic/simp_result): forgot to import in tactic.basic (#2462)
When I write a new tactic, I tend not to import it into `tactic.basic` or `tactic.interactive` while testing it and PR'ing it, to save having to recompile the whole library every time I tweak the tactic. But then, inevitably, I forget to add the import before the review process is finished. This imports `simp_result`, from #2356, into `tactic.basic`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
- Loading branch information