diff options
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 1d6278066a..6c903ce14e 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.") |