diff options
Diffstat (limited to 'ltac/g_obligations.ml4')
| -rw-r--r-- | ltac/g_obligations.ml4 | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4 index 987b9d5387..fd531ca691 100644 --- a/ltac/g_obligations.ml4 +++ b/ltac/g_obligations.ml4 @@ -18,6 +18,7 @@ open Constrexpr open Constrexpr_ops open Stdarg open Constrarg +open Tacarg open Extraargs let (set_default_tactic, get_default_tactic, print_default_tactic) = @@ -30,12 +31,23 @@ 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> *) module Gram = Pcoq.Gram -module Tactic = Pcoq.Tactic +module Tactic = Pltac open Pcoq @@ -66,6 +78,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 |