diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 11:52:19 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-15 11:52:19 +0200 |
| commit | 28c732ea340f5ac571a77a8ac26de600c29165b2 (patch) | |
| tree | 9ee6deb6ecb31c520ffb4c278560a527cb550db4 /plugins/ltac/extratactics.ml4 | |
| parent | e710306910afc61c9a874e6020bbf35b77ffe4af (diff) | |
| parent | 7668037a8daaef7bc8f1fc3225c2e6cc26cac0aa (diff) | |
Merge PR#375: Deprecation
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
0 files changed, 0 insertions, 0 deletions