diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 05fbd67cb..60f1a4749 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -46,8 +46,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env -> a [constr]. *) (** To embed several objects in Coqast.t *) -val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t - val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr val valueIn : value -> raw_tactic_arg |