diff options
| author | Pierre-Marie Pédrot | 2015-12-03 14:11:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-03 14:32:30 +0100 |
| commit | f5a752261f210e9c5ecbbbf54886904f0856975a (patch) | |
| tree | 5dd0abe451ba8f264074225f5500448e52376972 /tactics | |
| parent | fbb0d3151820517dee2f8e467435a6f045efbee0 (diff) | |
Removing the last use of tacticIn in setoid_ring.
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 |