diff options
| -rw-r--r-- | pretyping/tacred.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 5b150303c8..9f5dec3f34 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -964,7 +964,10 @@ let reduce_to_ref_gen allow_product env sigma ref t = try let t' = nf_betaiota (one_step_reduce env sigma t) in elimrec env t' l - with NotStepReducible -> raise Not_found + with NotStepReducible -> + errorlabstrm "" + (str "Not a statement of conclusion " ++ + Nametab.pr_global_env Idset.empty ref) in elimrec env t [] |