diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 8 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 483f82113d..ae7e2b79a8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1016,6 +1016,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (advance sigma self))) + (* compatibility *) let goal { self=self } = self diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 2157459f46..1a367f4eac 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -466,6 +466,10 @@ module Goal : sig (** Recover the list of current goals under focus, without evar-normalization *) val goals : [ `LZ ] t tactic list tactic + (** [unsolved g] is [true] if [g] is still unsolved in the current + proof state. *) + val unsolved : 'a t -> bool tactic + (** Compatibility: avoid if possible *) val goal : [ `NF ] t -> Evar.t |