diff options
| author | Hugo Herbelin | 2020-04-19 13:24:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-01 23:17:27 +0200 |
| commit | 653a06b843e380927b93e325dcbe1c339810406f (patch) | |
| tree | a14cdc52dd4f153477a42411480056349a1167e8 | |
| parent | df8df4637dfb4106854554cc2ac94b4fdd565e80 (diff) | |
Changing fixpoint message "decreasing" -> "guarded".
This is to be compatible with the possibility of having non truly
recursive fixpoints.
| -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 ())) |