diff options
| author | Pierre-Marie Pédrot | 2020-05-12 14:07:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-12 14:41:03 +0200 |
| commit | b3b967385830daa09a149e093fa6352a99884436 (patch) | |
| tree | 7deb98cedd6fce8b3a9f99610769d08809447092 /plugins/syntax/string_notation.ml | |
| parent | 5530ac6ee1fd533a2b56944bd9e16b0d767f3e61 (diff) | |
Clean up the legacy refiner implementation.
We avoid using global-access primitives and instead rely on purely functional
passing of the relevant data. Namely, we replace the goal argument with its
environment, and we pass the additional check parameter.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions