diff options
| author | Pierre-Marie Pédrot | 2020-05-24 18:13:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-25 08:05:39 +0200 |
| commit | a181ea2fce1177cc33cd7fdf504d69fff15c7e97 (patch) | |
| tree | e0c9183c9f88fe5b3fadbf9935ee237e74423451 /doc/plugin_tutorial/tuto2/src/custom.mli | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Remove the prolog tactic.
It was deprecated in 8.12 and not used in the wild.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/custom.mli')
0 files changed, 0 insertions, 0 deletions