diff options
Diffstat (limited to 'plugins/ltac/g_obligations.mlg')
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index d7918a58ac..c01b97c14d 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram open Obligations -let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac)) -let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac)) +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 _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF |