mathlib3
feat(tactic/terminal_goal): determine if other goals depend on the current one
#984

Merged

feat(tactic/terminal_goal): determine if other goals depend on the current one #984

mergify merged 11 commits into master from terminal_goal

feat(tactics): add "terminal_goal" tactic and relatives

5adcca38

fix(test/tactics): renaming test functions to avoid a name collision

6e405c42

fix(tactic): moving terminal_goal to tactic/basic.lean

6db334f3

fix(test/tactics): open tactics

92b835c4

touching a file, to prompt travis to try again

11f82093

Merge branch 'master' into terminal_goal

d580d0dd

merge and cleanup

8acd5706

terminal_goal

c7afd381

kim-em requested a review 6 years ago

fix

d2d93dfa

robertylewis dismissed these changes on 2019-05-14

merge

b184dce0

mergify dismissed their stale review 6 years ago

Pull request has been modified.

merge

589f86ec

robertylewis approved these changes on 2019-05-15

robertylewis assigned

robertylewis 6 years ago

robertylewis added ready-to-merge

mergify merged 3022cafd into master 6 years ago

mergify deleted the terminal_goal branch 6 years ago

Reviewers

robertylewis

Assignees

robertylewis

Labels

ready-to-merge

Milestone

No milestone