diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-27 10:58:45 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-02-27 10:58:45 +0100 |
| commit | 26134d1c4056b70b2bdadaf881ef951e5858b606 (patch) | |
| tree | f37d0e4f073a82cf877ee067b54906aebdc3f69a /tactics/tacinterp.ml | |
| parent | 64c53a3045187d766b379e9b0902912e0c0d310d (diff) | |
Dead code: eval_ltac_constr.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 52fb439c3..ad0ec0b59 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2105,14 +2105,6 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t let _ = Proof_global.set_interp_tac interp -let eval_ltac_constr t = - Proofview.tclUNIT () >= fun () -> (* delay for [make_empty_glob_sign] and [default_ist] *) - Proofview.Goal.enterl begin fun gl -> - interp_ltac_constr (default_ist ()) - (intern_tactic_or_tacarg (make_empty_glob_sign ()) t ) gl >= fun r -> - Proofview.Goal.return r - end - (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = |