Commit 2018-10-01 20:26 87a963be

feat(tactic/ext): add apply_cfg argument to ext1 (#346)

• feat(tactics/ext): use applyc _ {new_goals := new_goals.all} This causes goals to appear in the same order they appear as hypotheses of the @[extensionality] lemma, rather than being reordered to put dependent goals first. This doesn't appear to affect any uses of ext in mathlib, but is occasionally helpful in the development of category theory. (Indeed, I have been running into tactic mode proofs that fail to typecheck, when using ext, and this avoids the problem)
• adding configuration to non-interactive ext1 and a wrapper so tidy can sometimes produce shorter tactic scripts