mathlib3
fix(tactic/finish): fix one classical leak, document another
#1929

Merged

fix(tactic/finish): fix one classical leak, document another #1929

mergify merged 3 commits into leanprover-community:master from avigad:ifinish

fix(tactic/finish): fix one classical leak, document another

71588e0c

fix(src/tactic): deprecate intuitionistic versions in docstrings. Clo…

cea06fae

cipher1024 assigned

robertylewis 6 years ago

robertylewis approved these changes on 2020-01-30

robertylewis added ready-to-merge

Merge branch 'master' into ifinish

87696e70

mergify merged 9bc01784 into master 6 years ago

Reviewers

robertylewis

Assignees

robertylewis

Labels

ready-to-merge

Milestone

No milestone