diff options
| author | Pierre-Marie Pédrot | 2016-09-07 23:59:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 16:55:46 +0200 |
| commit | 52c3917be7239f7d5ab1ba882275b4571463f585 (patch) | |
| tree | 9458b71b44b5b04f649a054ace210b8382934dd3 /ltac | |
| parent | 1654b3989041b25e3b642ffde12125344342a54b (diff) | |
Making Proof_global terminator generic in external tactics.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_obligations.ml4 | 14 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 1 |
2 files changed, 14 insertions, 1 deletions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4 index 987b9d5387..db8daf32d1 100644 --- a/ltac/g_obligations.ml4 +++ b/ltac/g_obligations.ml4 @@ -30,6 +30,17 @@ let () = end in Obligations.default_tactic := tac +let with_tac f tac = + let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in + let tac = match tac with + | None -> None + | Some tac -> + let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in + let _, tac = Genintern.generic_intern env tac in + Some tac + in + f tac + (* We define new entries for programs, with the use of this module * Subtac. These entries are named Subtac.<foo> *) @@ -66,6 +77,9 @@ GEXTEND Gram open Obligations +let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac + let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 177867abd8..9e502682b8 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1969,7 +1969,6 @@ let interp_tac_gen lfun avoid_ids debug t = end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t -let _ = Proof_global.set_interp_tac interp (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) |