From e9d480b0bea05debefe3f52e5881ea7e00cef809 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 25 Jul 2014 12:01:37 +0200 Subject: Small reorganisation in proof.ml. --- proofs/proof.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'proofs/proof.ml') 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 -- cgit v1.2.3