diff options
| author | Pierre-Marie Pédrot | 2014-05-18 02:50:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-20 14:49:47 +0200 |
| commit | e705ae9d343c67212ce238899d21059ce93ee3e5 (patch) | |
| tree | 33eb5575b2da7275fdb13295243ef045afab3375 /intf | |
| parent | f79e9db4922f649d08153f09526d5c1c60a7e45c (diff) | |
Tentative to add constr-using primitive tactics without grammar rules.
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
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 |