diff options
| author | Arnaud Spiwack | 2014-02-27 10:58:45 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-27 10:58:45 +0100 |
| commit | 26134d1c4056b70b2bdadaf881ef951e5858b606 (patch) | |
| tree | f37d0e4f073a82cf877ee067b54906aebdc3f69a | |
| parent | 64c53a3045187d766b379e9b0902912e0c0d310d (diff) | |
Dead code: eval_ltac_constr.
| -rw-r--r-- | tactics/tacinterp.ml | 8 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
2 files changed, 0 insertions, 10 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 52fb439c31..ad0ec0b59d 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 = diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 6a236afda1..79b7f6fd52 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -103,8 +103,6 @@ val interp_tac_gen : value Id.Map.t -> Id.t list -> val interp : raw_tactic_expr -> unit Proofview.tactic -val eval_ltac_constr : raw_tactic_expr -> constr Proofview.glist Proofview.tactic - (** Hides interpretation for pretty-print *) val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic |