diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-14 11:39:24 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-14 18:02:41 -0500 |
| commit | a60a49f545499f29f067148668b8ec1bc7b55895 (patch) | |
| tree | 6dc6c4ec1c3f7e33c60f7a41cf1948c301a78f33 /plugins/ltac/tacinterp.ml | |
| parent | 29644bf0814945cbf2b4388b8f8bd19f109503a0 (diff) | |
Pass a ghost location for abstract
As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index dccb7cb75..73c0874d2 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1158,9 +1158,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end - | TacAbstract (loc,(t,ido)) -> + | TacAbstract (t,ido) -> let call = LtacMLCall tac in - push_trace(loc,call) ist >>= fun trace -> + push_trace(None,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:TacAbstract" trace (catch_error_tac trace begin Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT |