diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/library/declare.ml b/library/declare.ml index 1257044d3..ffe53e505 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -281,3 +281,37 @@ let declare_mind isrecord mie = !xml_declare_inductive (isrecord,oname); oname +(* Declaration messages *) + +let pr_rank i = str (ordinal (i+1)) + +let fixpoint_message indexes l = + Flags.if_verbose msgnl (match l with + | [] -> anomaly "no recursive definition" + | [id] -> pr_id id ++ str " is recursively defined" ++ + (match indexes with + | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)" + | _ -> mt ()) + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are recursively defined" ++ + match indexes with + | Some a -> spc () ++ str "(decreasing respectively on " ++ + prlist_with_sep pr_coma pr_rank (Array.to_list a) ++ + str " arguments)" + | None -> mt ())) + +let cofixpoint_message l = + Flags.if_verbose msgnl (match l with + | [] -> anomaly "No corecursive definition." + | [id] -> pr_id id ++ str " is corecursively defined" + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are corecursively defined")) + +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") + +let assumption_message id = + Flags.if_verbose msgnl (pr_id id ++ str " is assumed") |