diff --git a/test-suite/bugs/bug_4955.v b/test-suite/bugs/bug_4955.v index 74353a7eb210..611566aad2ba 100644 --- a/test-suite/bugs/bug_4955.v +++ b/test-suite/bugs/bug_4955.v @@ -32,7 +32,7 @@ Record Functor (C D : PreCategory) := Arguments object_of {C%_category D%_category} f%_functor c%_object : rename, simpl nomatch. Arguments morphism_of [C%_category] [D%_category] f%_functor [s%_object d%_object] -m%morphism : rename, simpl nomatch. +m%_morphism : rename, simpl nomatch. Section path_functor. Variable C : PreCategory. Variable D : PreCategory. diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index c5ade45e9083..34ed360b1e5e 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -59,6 +59,7 @@ let warn_arguments_assert = let warn_scope_delimiter_depth = CWarnings.create ~name:"argument-scope-delimiter" ~category:Deprecation.Version.v8_19 + ~default:AsError Pp.(fun () -> strbrk "The '%' scope delimiter in 'Arguments' commands is deprecated, " ++ strbrk "use '%_' instead (available since 8.19). The '%' syntax will be " ++