diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index c386ac6aa8..b0c1f0cc54 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -282,7 +282,7 @@ let declare_mind isrecord mie = let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = - Flags.if_verbose msgnl (match l with + Flags.if_verbose msg_info (match l with | [] -> anomaly "no recursive definition" | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with @@ -297,7 +297,7 @@ let fixpoint_message indexes l = | None -> mt ())) let cofixpoint_message l = - Flags.if_verbose msgnl (match l with + Flags.if_verbose msg_info (match l with | [] -> anomaly "No corecursive definition." | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -307,7 +307,7 @@ let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose msgnl (pr_id id ++ str " is defined") + Flags.if_verbose msg_info (pr_id id ++ str " is defined") let assumption_message id = - Flags.if_verbose msgnl (pr_id id ++ str " is assumed") + Flags.if_verbose msg_info (pr_id id ++ str " is assumed") |