diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-25 12:01:37 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-25 12:08:07 +0200 |
commit | e9d480b0bea05debefe3f52e5881ea7e00cef809 (patch) | |
tree | 72783af7230f09205efa6c72d5b4b437a08fe950 /proofs/proof.ml | |
parent | 5a57af79612dded92c43f9c43ad20d894974328a (diff) |
Small reorganisation in proof.ml.
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r-- | proofs/proof.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 98876a435..067111d59 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -61,6 +61,9 @@ exception CannotUnfocusThisWay (* Cannot focus on non-existing subgoals *) exception NoSuchGoals of int * int + +exception FullyUnfocused + let _ = Errors.register_handler begin function | CannotUnfocusThisWay -> Errors.error "This proof is focused, but cannot be unfocused this way" @@ -70,6 +73,7 @@ let _ = Errors.register_handler begin function Errors.errorlabstrm "Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) + | FullyUnfocused -> Errors.error "The proof is not focused" | _ -> raise Errors.Unhandled end @@ -152,11 +156,6 @@ let partial_proof p = Proofview.partial_proof p.entry p.proofview let push_focus cond inf context pr = { pr with focus_stack = (cond,inf,context)::pr.focus_stack } -exception FullyUnfocused -let _ = Errors.register_handler begin function - | FullyUnfocused -> Errors.error "The proof is not focused" - | _ -> raise Errors.Unhandled -end (* An auxiliary function to read the kind of the next focusing step *) let cond_of_focus pr = match pr.focus_stack with |