mathlib3
feat(tactics/interactive): choose uses exists_prop
#1014

Merged

feat(tactics/interactive): choose uses exists_prop #1014

mergify merged 5 commits into master from choose

feat(tactics/interactive): choose uses exists_prop

8ec92dc6

PatrickMassot requested a review 6 years ago

Merge branch 'master' into choose

3538efb8

fix build

05632141

cipher1024 approved these changes on 2019-05-13

cipher1024 added ready-to-merge

Merge branch 'master' into 'choose'

82790f08

Merge branch 'master' into 'choose'

c3ab3b24

mergify merged 01b345c1 into master 6 years ago

mergify deleted the choose branch 6 years ago

Reviewers

cipher1024

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone