diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 7fa6c5fee8..264cd139e1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -98,20 +98,20 @@ let hypothesis_def_var is_refining ident n c = let minductive_message = function | [] -> anomaly "no inductive definition" - | [x] -> [< print_id x; 'sTR " is defined">] - | l -> hOV 0 [< prlist_with_sep pr_coma print_id l; + | [x] -> [< pr_id x; 'sTR " is defined">] + | l -> hOV 0 [< prlist_with_sep pr_coma pr_id l; 'sPC; 'sTR "are defined">] let recursive_message = function | [] -> anomaly "no recursive definition" - | [x] -> [< print_id x; 'sTR " is recursively defined">] - | l -> hOV 0 [< prlist_with_sep pr_coma print_id l; + | [x] -> [< pr_id x; 'sTR " is recursively defined">] + | l -> hOV 0 [< prlist_with_sep pr_coma pr_id l; 'sPC; 'sTR "are recursively defined">] let corecursive_message = function | [] -> anomaly "no corecursive definition" - | [x] -> [< print_id x; 'sTR " is corecursively defined">] - | l -> hOV 0 [< prlist_with_sep pr_coma print_id l; + | [x] -> [< pr_id x; 'sTR " is corecursively defined">] + | l -> hOV 0 [< prlist_with_sep pr_coma pr_id l; 'sPC; 'sTR "are corecursively defined">] let build_mutual lparams lnamearconstrs finite = |