From 3dc37b55102cc8f23299c175cdce2d4e980f0d53 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 29 Nov 2004 18:32:09 +0000
Subject: UserError in reduce_to_*_ref

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

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5b150303c..9f5dec3f3 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 []
 
-- 
cgit v1.2.3