diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 754ad8526..cdeecf1bb 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -609,8 +609,7 @@ let declare_mutual_inductive_with_eliminations mie impls = begin match mie.mind_entry_finite with | BiFinite when is_recursive mie -> if Option.has_some mie.mind_entry_record then - error ("Records declared with the keywords Record or Structure cannot be recursive." ^ - "You can, however, define recursive records using the Inductive or CoInductive command.") + error "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command." else error ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.") | _ -> () @@ -697,19 +696,19 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - Id.to_string y^" depends on "^Id.to_string x^" but not conversely" + pr_id y ++ str " depends on " ++ pr_id x ++ str " but not conversely" else if Id.List.mem y xge then - Id.to_string x^" depends on "^Id.to_string y^" but not conversely" + pr_id x ++ str " depends on " ++ pr_id y ++ str " but not conversely" else - Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in - let e = if List.is_empty rest then reason else "e.g.: "^reason in + pr_id y ++ str " and " ++ pr_id x ++ str " are not mutually dependent" in + let e = if List.is_empty rest then reason else str "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = if isfix - then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() + then str "Well-foundedness check may fail unexpectedly." ++ fnl() else mt () in - strbrk ("Not a fully mutually defined "^k) ++ fnl () ++ - strbrk ("("^e^").") ++ fnl () ++ w + str "Not a fully mutually defined " ++ str k ++ fnl () ++ + str "(" ++ e ++ str ")." ++ fnl () ++ w let check_mutuality env isfix fixl = let names = List.map fst fixl in |