diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index efe62f569c..0c2b754788 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -251,6 +251,10 @@ and 'a gen_tactic_expr = 'a gen_tactic_expr | TacExactlyOnce of 'a gen_tactic_expr + | TacIfThenCatch of + 'a gen_tactic_expr * + 'a gen_tactic_expr * + 'a gen_tactic_expr | TacOrelse of 'a gen_tactic_expr * 'a gen_tactic_expr |