Algebraized "No such hypothesis" errors

7 files changed, 14 insertions, 10 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
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index da8f2668b8..c5017ac75b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -124,7 +124,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
      match Tacmach.pf_hyps gl with
         (last_hyp_id,_,_)::_ -> last_hyp_id
       | _ -> (* even the hypothesis id is missing *)
-             error ("No such hypothesis: " ^ (Id.to_string !id) ^".")
+        raise (Logic.RefinerError (Logic.NoSuchHyp !id))
     in
     let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in
     let gls = gl'.Evd.it in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 712191a736..4f7a6188a7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -350,8 +350,7 @@ let interp_hyp ist env (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else user_err_loc (loc,"eval_variable",
-    str "No such hypothesis: " ++ pr_id id ++ str ".")
+  else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id))
 
 let interp_hyp_list_as_list ist env (loc,id as x) =
   try coerce_to_hyp_list env (Id.Map.find id ist.lfun)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8546b03a17..be6461de1a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -523,7 +523,7 @@ let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac =
   aux []
 
 let rec get_next_hyp_position id = function
-  | [] -> error ("No such hypothesis: " ^ Id.to_string id)
+  | [] -> raise (RefinerError (NoSuchHyp id))
   | (hyp,_,_) :: right ->
       if Id.equal hyp id then
 	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8df362f3ac..1cbb47846c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -928,6 +928,9 @@ let explain_meta_in_type c =
   str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_lconstr c ++
   str " of another meta"
 
+let explain_no_such_hyp id =
+  str "No such hypothesis: " ++ pr_id id
+
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
   | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
@@ -937,6 +940,7 @@ let explain_refiner_error = function
   | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
   | NonLinearProof c -> explain_non_linear_proof c
   | MetaInType c -> explain_meta_in_type c
+  | NoSuchHyp id -> explain_no_such_hyp id
 
 (* Inductive errors *)