diff options
| author | Pierre-Marie Pédrot | 2014-01-06 14:39:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-06 14:39:53 +0100 |
| commit | 2f6e3a8a453c3fa29bbc660a929c5140916c76b3 (patch) | |
| tree | c7ab6e7576cbbb4adde5404183c062ef697a7389 /proofs | |
| parent | 0427f99bd793a8aa8245e61ec340ca4c6966ba63 (diff) | |
Algebraized "No such hypothesis" errors
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 8 | ||||
| -rw-r--r-- | proofs/logic.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
3 files changed, 7 insertions, 6 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 516c90daa9..60548ef7da 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -37,6 +37,7 @@ type refiner_error = (* Errors raised by the tactics *) | IntroNeedsProduct | DoesNotOccurIn of constr * Id.t + | NoSuchHyp of Id.t exception RefinerError of refiner_error @@ -68,8 +69,7 @@ let rec catchable_exception = function (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false -let error_no_such_hypothesis id = - error ("No such hypothesis: " ^ Id.to_string id ^ ".") +let error_no_such_hypothesis id = raise (RefinerError (NoSuchHyp id)) (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) @@ -81,13 +81,13 @@ let with_check = Flags.with_option check let apply_to_hyp sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if !check then error "No such assumption." + if !check then error_no_such_hypothesis id else sign let apply_to_hyp_and_dependent_on sign id f g = try apply_to_hyp_and_dependent_on sign id f g with Hyp_not_found -> - if !check then error "No such assumption." + if !check then error_no_such_hypothesis id else sign let check_typability env sigma c = diff --git a/proofs/logic.mli b/proofs/logic.mli index eff766b7c5..69c10812ab 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -48,6 +48,7 @@ type refiner_error = (*i Errors raised by the tactics i*) | IntroNeedsProduct | DoesNotOccurIn of constr * Id.t + | NoSuchHyp of Id.t exception RefinerError of refiner_error diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index ae0d1039b6..c0875d756f 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -53,7 +53,7 @@ let pf_get_hyp gls id = try Context.lookup_named id (pf_hyps gls) with Not_found -> - error ("No such hypothesis: " ^ (Id.to_string id)) + raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = let (_,_,ty)= (pf_get_hyp gls id) in @@ -234,7 +234,7 @@ module New = struct let hyps = Proofview.Goal.hyps gl in let sign = try Context.lookup_named id hyps - with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id)) + with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign |