diff options
| author | herbelin | 2003-03-31 21:18:53 +0000 |
|---|---|---|
| committer | herbelin | 2003-03-31 21:18:53 +0000 |
| commit | 00608fac2d8e217232d5f2ddd28a43971bf259b7 (patch) | |
| tree | 0bd65009594d83c85a6e3f4f5bf8a0e77e0b4fc6 /contrib/funind | |
| parent | ca29570a25be8f9b8757399f5f0b72b4a9bd5e43 (diff) | |
Ajout d'un message à FailTac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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) |