diff options
| author | Gaëtan Gilbert | 2018-10-29 14:34:39 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-30 13:04:18 +0100 |
| commit | 82105f030e13aebcb232eb912526ff8ca0650a24 (patch) | |
| tree | 9839e8698063b8e55f4255efdabcceed2e8deea3 /plugins | |
| parent | 0ac673e562c34245e4e48efc428d808e917be79b (diff) | |
Move abstract out of tactics.ml
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index b660865e8b..05a65e4cd8 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -855,9 +855,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } END (* ********************************************************************* *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b60b77595b..eecb2ac6de 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1078,7 +1078,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with 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 + Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) end end) | TacThen (t1,t) -> |