diff options
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 0d355890c5..8bbd82bb0a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -488,3 +488,12 @@ module V82 = struct { pr with proofview ; shelf } end + +let all_goals p = + let add gs set = + List.fold_left (fun s g -> Goal.Set.add g s) set gs in + let (goals,stack,shelf,given_up,_) = proof p in + let set = add goals Goal.Set.empty in + let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in + let set = add shelf set in + add given_up set |