diff options
| author | Hugo Herbelin | 2020-08-19 20:29:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-19 20:35:28 +0200 |
| commit | 3c45a14684d48c093a7f3820b57d4fa37dbc0b99 (patch) | |
| tree | ea2e089c55a7cece15b9930b2903a7075a13203f /dev/ci/docker | |
| parent | daed771ff18978dea536b277e00c0ca0149129ee (diff) | |
In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API.
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions