diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:24:27 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 11:24:27 +0100 |
| commit | c5432539927de8a94d5c549d288b95b7215390b9 (patch) | |
| tree | a894769d27c70c780f684ff63b5e547556186a91 /plugins/rtauto/proof_search.ml | |
| parent | 76058420ec0ea037504adf0af213d0542bd7c1c3 (diff) | |
| parent | ba0a37d773c5d42f96b3b88714767ba2e7fb7a3b (diff) | |
Merge PR #6909: Deprecate Focus and Unfocus
Diffstat (limited to 'plugins/rtauto/proof_search.ml')
0 files changed, 0 insertions, 0 deletions