diff options
| author | Théo Zimmermann | 2016-10-03 13:57:16 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2016-10-03 17:03:39 +0200 |
| commit | 3be2307af0f1316630b46078fd6b4367c283472d (patch) | |
| tree | 4703d22f190d73b119d635fd4b15bdb706d8523d /plugins/syntax/string_syntax_plugin.mllib | |
| parent | 89ec88f1e750cfb786de1929ef44fac70c9a29ab (diff) | |
Remove if_then_else. Use tryif instead.
if_then_else definition does not account for multi success tactics.
tryif_then_else is a primitive tactical with the expected behavior.
Diffstat (limited to 'plugins/syntax/string_syntax_plugin.mllib')
0 files changed, 0 insertions, 0 deletions