diff options
| -rw-r--r-- | vernac/declare.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/declare.ml b/vernac/declare.ml index 357f58feea..f9b8019b45 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -580,12 +580,12 @@ let fixpoint_message indexes l = | [] -> CErrors.anomaly (Pp.str "no recursive definition.") | [id] -> Id.print id ++ str " is recursively defined" ++ (match indexes with - | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | Some [|i|] -> str " (guarded on "++pr_rank i++str " argument)" | _ -> mt ()) | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ spc () ++ str "are recursively defined" ++ match indexes with - | Some a -> spc () ++ str "(decreasing respectively on " ++ + | Some a -> spc () ++ str "(guarded respectively on " ++ prvect_with_sep pr_comma pr_rank a ++ str " arguments)" | None -> mt ())) |