From ace68194290b49c459a56ea0a023863056fae0e2 Mon Sep 17 00:00:00 2001
From: jforest
Date: Fri, 13 Jul 2007 10:36:24 +0000
Subject: removing a warning at compilation time

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

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index afbe1c933d..31c9659b10 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -1415,7 +1415,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       with e -> 
 	begin 
 	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
-	  then anomalylabstrm "" (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e)
+	  then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
 (* 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
-- 
cgit v1.2.3