diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 51d66a761..12ce73a5b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -91,7 +91,7 @@ let interp_definition bl red_option c ctypopt = let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in (* Check that all implicit arguments inferable from the term is inferable from the type *) if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false) - then warn (str "Implicit arguments declaration relies on type." ++ + then msg_warning (str "Implicit arguments declaration relies on type." ++ spc () ++ str "The term declares more implicits than the type here."); imps1@(Impargs.lift_implicits nb_args impsty), { const_entry_body = body; |