diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3e8c71482..bcd9d6e0d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -281,6 +281,21 @@ let close_proof () = | Proof.HasUnresolvedEvar -> Util.error "Attempt to save a proof with existential variables still non-instantiated" + +(**********************************************************) +(* *) +(* Utility functions *) +(* *) +(**********************************************************) + +let maximal_unfocus k p = + begin try while Proof.no_focused_goal p do + Proof.unfocus k p + done + with Util.UserError _ -> (* arnaud: attention à ça si je fini par me décider à mettre une vrai erreur pour Proof.unfocus *) + () + end + module V82 = struct let get_current_initial_conclusions () = let p = give_me_the_proof () in |