From 9c1e76422c63ab845d72893ca85dd38ce5ce9bec Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 14 Aug 2014 13:00:34 +0200
Subject: Restore the error-handling behavior of [change], which was silently
 failing when conversion in the goal failed.

---
 tactics/tactics.ml | 9 +++------
 1 file 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)
-- 
cgit v1.2.3