Skip to content

Commit efc9633

Browse files
committed
Make argument-scope-delimiter error by default
In order to actually handle this 8.19 deprecation in 9.4.
1 parent 93c35c9 commit efc9633

File tree

2 files changed

+2
-1
lines changed

2 files changed

+2
-1
lines changed

test-suite/bugs/bug_4955.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ Record Functor (C D : PreCategory) :=
3232
Arguments object_of {C%_category D%_category} f%_functor c%_object : rename, simpl
3333
nomatch.
3434
Arguments morphism_of [C%_category] [D%_category] f%_functor [s%_object d%_object]
35-
m%morphism : rename, simpl nomatch.
35+
m%_morphism : rename, simpl nomatch.
3636
Section path_functor.
3737
Variable C : PreCategory.
3838
Variable D : PreCategory.

vernac/comArguments.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ let warn_arguments_assert =
5959

6060
let warn_scope_delimiter_depth =
6161
CWarnings.create ~name:"argument-scope-delimiter" ~category:Deprecation.Version.v8_19
62+
~default:AsError
6263
Pp.(fun () ->
6364
strbrk "The '%' scope delimiter in 'Arguments' commands is deprecated, " ++
6465
strbrk "use '%_' instead (available since 8.19). The '%' syntax will be " ++

0 commit comments

Comments
 (0)