diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 14 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 18 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6651e49652..eaaa1f7c30 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -826,6 +826,20 @@ module Goal = struct tclZERO e end + let goals = + Proof.current >>= fun env -> + Proof.get >>= fun step -> + let sigma = step.solution in + let map goal = + match Goal.advance sigma goal with + | None -> None (** ppedrot: Is this check really necessary? *) + | Some goal -> + (** The sigma is unchanged. *) + let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in + Some gl + in + tclUNIT (List.map_filter map step.comb) + (* compatibility *) let goal { self=self } = self let refresh_sigma g = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 6177803c78..c27e4ba1a9 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -370,8 +370,12 @@ module Goal : sig each goal. *) val enter : ([ `NF ] t -> unit tactic) -> unit tactic + (** Same as enter, but does not normalize the goal beforehand. *) val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic + (** Recover the list of current goals under focus *) + val goals : [ `NF ] t list tactic + (* compatibility: avoid if possible *) val goal : [ `NF ] t -> Goal.goal |