diff options
| author | Pierre-Marie Pédrot | 2019-05-13 00:26:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-15 00:20:40 +0200 |
| commit | 3cdaffab75414f3f59386a4b76c6b00c94bc8b0e (patch) | |
| tree | 822d2dee865ba8801592f153223bb5ad0bd38aa4 /engine/ftactic.ml | |
| parent | e74fce3090323b4d3734f84ee8cf6dc1f5e85953 (diff) | |
Simplify the private constant API.
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
Diffstat (limited to 'engine/ftactic.ml')
0 files changed, 0 insertions, 0 deletions