mathlib3
refactor(tactic/interactive): remove dependencies of
#878

Merged

refactor(tactic/interactive): remove dependencies of #878

mergify merged 3 commits into master from split-interactive

cipher1024 assigned

digama0 6 years ago

cipher1024 force pushed from 4beaf608 to 6d66b2ff 6 years ago

cipher1024 requested a review 6 years ago

cipher1024 force pushed from 6d66b2ff to a64d32a2 6 years ago

cipher1024 force pushed from a64d32a2 to b5291a2e 6 years ago

cipher1024 force pushed from 5209ca29 to ad9eaf80 6 years ago

kim-em commented on 2019-04-16

cipher1024 force pushed from 375ae922 to 42fc970c 6 years ago

cipher1024 force pushed from 42fc970c to f32634f1 6 years ago

digama0 commented on 2019-04-21

robertylewis dismissed these changes on 2019-04-21

mergify dismissed their stale review 6 years ago

Pull request has been modified.

cipher1024 force pushed from 75623391 to 2b95f1ab 6 years ago

cipher1024 force pushed from 2b95f1ab to b933bd13 6 years ago

cipher1024 force pushed from b933bd13 to 0f623156 6 years ago

cipher1024 force pushed from bd346134 to ae381e3b 6 years ago

refactor(tactic/interactive): remove dependencies of

ff8fa46d

cipher1024 force pushed from ae381e3b to ff8fa46d 6 years ago

jcommelin approved these changes on 2019-04-29

cipher1024 added ready-to-merge

Merge branch 'master' into 'split-interactive'

025e3b37

digama0 commented on 2019-04-29

digama0 approved these changes on 2019-04-29

cipher1024 removed ready-to-merge

cipher1024 added ready-to-merge

Merge branch 'master' into 'split-interactive'

0d67acab

mergify merged 00aaf05a into master 6 years ago

cipher1024 deleted the split-interactive branch 6 years ago

Reviewers

digama0

jcommelin

robertylewis

kim-em

Assignees

digama0

Labels

ready-to-merge

Milestone

No milestone

mathlib3 refactor(tactic/interactive): remove dependencies of #878 Merged

refactor(tactic/interactive): remove dependencies of #878

mathlib3
refactor(tactic/interactive): remove dependencies of
#878

Merged