diff options
| author | Gaëtan Gilbert | 2020-10-09 21:51:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-26 14:41:39 +0100 |
| commit | 5146b2f01b3b901ac99823d3a448c77560f248db (patch) | |
| tree | 135ce50f8d5ff9cc24e7101ca3b0c2cecb4da182 /lib/objFile.ml | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Improve tactic interpreter registration API a bit
Using it feels nicer this way, with GADT details hidden inside comtactic
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions