That Function is unable to create a Fixpoint equation is a user problem,

not an anomaly

1 files changed, 3 insertions, 1 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62f3071151..fa84e4ddf3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1538,7 +1538,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
 	begin
 	  if do_observe ()
 	  then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e)
-	  else anomaly (Pp.str "Cannot create equation Lemma")
+	  else CErrors.errorlabstrm "Cannot create equation Lemma"
+               (str "Cannot create equation lemma." ++ spc () ++ 
+                str "This may be because the function is nested-recursive.")
 	  ;
 	  true
 	end