Restore the error-handling behavior of [change], which was silently failing

when conversion in the goal failed.

1 files changed, 3 insertions, 6 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c2b7351bd2..18d9acf639 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -375,20 +375,17 @@ let change_and_check cv_pb t env sigma c =
   let sigma, t' = t env sigma in
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
     if b then sigma, t'
-    else raise ConstrMatching.PatternMatchingFailure
+    else errorlabstrm "convert-check-hyp" (str "Not convertible.")
 
 let change_and_check_subst cv_pb subst t env sigma c =
   let t' env sigma = 
     let sigma, t = t env sigma in
       sigma, replace_vars (Id.Map.bindings subst) t 
   in change_and_check cv_pb t' env sigma c
-      
+
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
-  | None -> fun env sigma c ->
-    (try change_and_check cv_pb t env sigma c
-     with ConstrMatching.PatternMatchingFailure ->
-       errorlabstrm "convert-check-hyp" (str "Not convertible."))
+  | None -> change_and_check cv_pb t
   | Some occl ->
     e_contextually false occl
       (fun subst -> change_and_check_subst Reduction.CONV subst t)