diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 1071605fc..9267e236d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -147,7 +147,7 @@ let declare_definition ident (local, k) ce imps hook = let () = if Pfedit.refining () then let msg = strbrk "Section definition " ++ pr_id ident ++ strbrk " is not visible from current goals" in - Flags.if_warn msg_warning msg + msg_warning msg in VarRef ident | Discharge | Local | Global -> @@ -503,7 +503,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_warn msg_warning (non_full_mutual_message x xge y yge isfix rest) + msg_warning (non_full_mutual_message x xge y yge isfix rest) | _ -> () type structured_fixpoint_expr = { |