diff options
| author | Guillaume Melquiond | 2015-12-16 18:30:32 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-16 18:30:32 +0100 |
| commit | b8d1e84e9326df34383e5e5c8c5842cb7013b935 (patch) | |
| tree | d3783da15f09d47b1002b2ed31385f897e8bd4bf /plugins/syntax/string_syntax.ml | |
| parent | 53ab313dcf7ae524a9a8312658c1e9869a4039f7 (diff) | |
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions