diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 1 |
2 files changed, 0 insertions, 7 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2597606aa1..1928b44b47 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2389,12 +2389,6 @@ let interp_redexp env sigma r = (* Embed tactics in raw or glob tactic expr *) let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t)) -let tacticIn t = - globTacticIn (fun ist -> - try glob_tactic (t ist) - with e when Errors.noncritical e -> anomaly ~label:"tacticIn" - (str "Incorrect tactic expression. Received exception is:" ++ - Errors.print e)) (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 60f1a47492..60c9dc43e4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -46,7 +46,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env -> a [constr]. *) (** To embed several objects in Coqast.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 |