diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-25 09:42:03 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-25 09:48:19 +0200 |
| commit | 95429d01a8f47f5f9d1ecee3b452d920e1e1af22 (patch) | |
| tree | fde226fd665d9b6415720765423ff7aca1393c42 /plugins/funind/recdef.ml | |
| parent | 8232f27773f3463600fbaac0f70966bd4893ea20 (diff) | |
| parent | a7996005f57c12ba8fbb22c61ad97ac872da9d83 (diff) | |
Merge commit 'a799600' into v8.6
Was PR#334: Fix bug 5031 : should not be an anomaly
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 |