From a7f6af588068c7e8a7d38e152df0d9139338311b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 30 Jul 2010 08:47:08 +0000
Subject: Capitulation wrt "change pat with term": instead of solving the
 problem raised by taral on coq-club

  Goal forall X : Prop, X -> False -> False.
  intro. change (?t -> False) with (not t).

we just fail with an error message of "mauvaise foi".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13360 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 94ea43f45d..1957f04751 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2421,7 +2421,9 @@ and interp_atomic ist gl tac =
   | TacChange (Some op,c,cl) ->
       let sign,op = interp_typed_pattern ist env sigma op in
       h_change (Some op)
-        (pf_interp_constr ist (extend_gl_hyps gl sign) c)
+        (try pf_interp_constr ist (extend_gl_hyps gl sign) c
+	 with Not_found | Anomaly _ (* Hack *) ->
+	   errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side."))
         (interp_clause ist gl cl)
 
   (* Equivalence relations *)
-- 
cgit v1.2.3