From 00608fac2d8e217232d5f2ddd28a43971bf259b7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 21:18:53 +0000
Subject: Ajout d'un message à FailTac

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/tacinv.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/funind')

diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 6bc310460d..3137a38ad1 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -528,7 +528,7 @@ let rec iterintro i =
         let hypname = (string_of_id (destVar hyp)) in
         let sub = 
          try String.sub hypname 0 4 with _ -> "" (* different than "_eq_" *) in
-        if sub="_eq_" then rewriteLR hyp else tclFAIL 0)
+        if sub="_eq_" then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
       )) gl)
 
 
-- 
cgit v1.2.3