diff options
| author | Pierre-Marie Pédrot | 2020-10-21 14:18:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-04 17:53:02 +0100 |
| commit | f661944a302a024f1120212c21c093a7dae67642 (patch) | |
| tree | 1e6674770a590ee93b84405821cfd4b707e97ba4 /plugins/syntax/numeral_notation_plugin.mlpack | |
| parent | 7f90e6e0aa8dd27c64bac0dbc4b247ebb33d4aca (diff) | |
Adding an if-then-else syntax to Ltac2.
This is a syntactic sugar that is compiled away to a simple case analysis.
Diffstat (limited to 'plugins/syntax/numeral_notation_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions