From a7996005f57c12ba8fbb22c61ad97ac872da9d83 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Mon, 24 Oct 2016 08:48:05 +0200 Subject: That Function is unable to create a Fixpoint equation is a user problem, not an anomaly --- plugins/funind/recdef.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62f307115..fa84e4ddf 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 -- cgit v1.2.3