diff options
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) |