diff options
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 |