diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-30 09:50:48 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-30 10:54:42 +0200 |
| commit | 627659dd1449d4521132efb1f01ad57b128b235c (patch) | |
| tree | c1f143c75e5adbfb6e1e702bca5462d64e54344c /toplevel | |
| parent | 1b2d1628dfa52e6c1a5a0c328b80829b03cea58f (diff) | |
Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl
Diffstat (limited to 'toplevel')
| -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 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.") |