From 627659dd1449d4521132efb1f01ad57b128b235c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Sep 2016 09:50:48 +0200 Subject: Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl --- toplevel/vernacentries.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'toplevel') diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1d6278066..6c903ce14 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -980,7 +980,8 @@ let warn_arguments_assert = strbrk "If you want to clear notation scopes add ': clear scopes'") let warn_renaming_nonimplicit = - CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + CWarnings.create ~name:"arguments-ignore-rename-nonimpl" + ~category:"vernacular" (fun (oldn, newn) -> strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++ strbrk ". Only implicit arguments can be renamed.") -- cgit v1.2.3