diff options
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2095.v | 19 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2108.v | 22 | ||||
-rw-r--r-- | toplevel/command.ml | 9 |
3 files changed, 47 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2095.v b/test-suite/bugs/closed/shouldsucceed/2095.v new file mode 100644 index 000000000..28ea99dfe --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2095.v @@ -0,0 +1,19 @@ +(* Classes and sections *) + +Section OPT. + Variable A: Type. + + Inductive MyOption: Type := + | MyNone: MyOption + | MySome: A -> MyOption. + + Class Opt: Type := { + f_opt: A -> MyOption + }. +End OPT. + +Definition f_nat (n: nat): MyOption nat := MySome _ n. + +Instance Nat_Opt: Opt nat := { + f_opt := f_nat +}. diff --git a/test-suite/bugs/closed/shouldsucceed/2108.v b/test-suite/bugs/closed/shouldsucceed/2108.v new file mode 100644 index 000000000..cad8baa98 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2108.v @@ -0,0 +1,22 @@ +(* Declare Module in Module Type *) +Module Type A. +Record t : Set := { something : unit }. +End A. + + +Module Type B. +Declare Module BA : A. +End B. + + +Module Type C. +Declare Module CA : A. +Declare Module CB : B with Module BA := CA. +End C. + + +Module Type D. +Declare Module DA : A. +(* Next line gives: "Anomaly: uncaught exception Not_found. Please report." *) +Declare Module DC : C with Module CA := DA. +End D. 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 = { |