diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-12 17:53:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-12 17:53:24 +0000 |
| commit | deec843772d392f71806c011351fa6d4f551115d (patch) | |
| tree | 281314ec77155b7804af0636a3bd5290baaf29e2 /toplevel | |
| parent | 9df6e882d61ae9c1502d9f3e81e2bf304fa6679e (diff) | |
Added regression tests for bugs + miscellaneous improvements
- #2095 (not fixed in v8.2 but fixed in v8.3 and trunk)
- #2108 (fixed in v8.2, v8.3, trunk)
- #2102 (moved warning to msg_warning to ensure flushing, but still
open enhancement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13121 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index d20c213c4..8d840a458 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -426,8 +426,11 @@ let non_full_mutual_message x xge y yge isfix rest = let e = if rest <> [] then "e.g.: "^reason else reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = - if isfix then "Well-foundedness check may fail unexpectedly.\n" else "" in - "Not a fully mutually defined "^k^"\n("^e^").\n"^w + if isfix + then strbrk "Well-foundedness check may fail unexpectedly." ++ fnl() + else mt () in + strbrk ("Not a fully mutually defined "^k) ++ fnl () ++ + strbrk ("("^e^").") ++ fnl () ++ w let check_mutuality env isfix fixl = let names = List.map fst fixl in @@ -438,7 +441,7 @@ let check_mutuality env isfix fixl = let po = partial_order preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with | (x,Inr xge)::(y,Inr yge)::rest -> - if_verbose warning (non_full_mutual_message x xge y yge isfix rest) + if_verbose msg_warning (non_full_mutual_message x xge y yge isfix rest) | _ -> () type structured_fixpoint_expr = { |