diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 532786fd37..5a7a20ef63 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -106,19 +106,14 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacIntrosUntil of quantified_hypothesis | TacIntroMove of Id.t option * 'nam move_location | TacExact of 'trm - | TacExactNoCheck of 'trm - | TacVmCastNoCheck of 'trm | TacApply of advanced_flag * evars_flag * 'trm with_bindings list * ('nam * intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings * 'trm with_bindings option - | TacElimType of 'trm | TacCase of evars_flag * 'trm with_bindings - | TacCaseType of 'trm | TacFix of Id.t option * int | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list - | TacCut of 'trm | TacAssert of ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option * intro_pattern_expr located option * 'trm @@ -136,7 +131,6 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacDecomposeOr of 'trm | TacDecompose of 'ind list * 'trm | TacSpecialize of int option * 'trm with_bindings - | TacLApply of 'trm (* Automation tactics *) | TacTrivial of debug * 'trm list * string list option |