mathlib3
fix(tactic/elide): was untested and buggy. Fixed a few issues
#1638

Merged

fix(tactic/elide): was untested and buggy. Fixed a few issues #1638

mergify merged 5 commits into master from fix-elide

fix(tactic/elide): was untested and buggy. Fixed a few issues

e036865a

Update tactics.lean

84096075

robertylewis commented on 2019-10-31

add copyright header

0d12b236

Update src/tactic/elide.lean

284c5633

robertylewis approved these changes on 2019-10-31

robertylewis added ready-to-merge

Merge branch 'master' into fix-elide

c1016de8

mergify merged 5f17abcc into master 6 years ago

mergify deleted the fix-elide branch 6 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone