diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 18 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 |
2 files changed, 19 insertions, 2 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6651e49652..b32b1d62db 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -826,6 +826,21 @@ module Goal = struct tclZERO e end + let goals = + let (>>=) = Proof.bind in + Proof.current >>= fun env -> + Proof.get >>= fun step -> + let map goal = + let goal = Goal.advance step.solution goal in + match goal with + | None -> None + | Some g -> + let (t, _) = Goal.eval (enter_t (fun x -> x)) env step.solution g in + Some t + in + let goals = List.map_filter map step.comb in + Proof.ret goals + (* compatibility *) let goal { self=self } = self let refresh_sigma g = @@ -861,5 +876,4 @@ end module NonLogical = Proofview_monad.NonLogical let tclLIFT = Proofview_monad.Logical.lift - - +let tclGOALS = Goal.goals diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6177803c78..769bfb001f 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -453,3 +453,6 @@ end (* [tclLIFT c] includes the non-logical command [c] in a tactic. *) val tclLIFT : 'a NonLogical.t -> 'a tactic + +(* Access the current goals *) +val tclGOALS : [ `NF ] Goal.t list tactic |