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 /user-contrib/Ltac2/tac2expr.mli | |
| 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 'user-contrib/Ltac2/tac2expr.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2expr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index 548655f561..0ae016265a 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -105,6 +105,7 @@ type raw_tacexpr_r = | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr | CTacCnv of raw_tacexpr * raw_typexpr | CTacSeq of raw_tacexpr * raw_tacexpr +| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr | CTacCse of raw_tacexpr * raw_taccase list | CTacRec of raw_recexpr | CTacPrj of raw_tacexpr * ltac_projection or_relid |