diff --git a/doc/changelog/03-notations/19653-fix-19541.rst b/doc/changelog/03-notations/19653-fix-19541.rst new file mode 100644 index 0000000000..63de9b4363 --- /dev/null +++ b/doc/changelog/03-notations/19653-fix-19541.rst @@ -0,0 +1,6 @@ +- **Fixed:** + spurious warning about incompatible prefixes in presence of ``as + pattern`` :n:`@syntax_modifier` + (`#19653 `_, + fixes `#19541 `_, + by Pierre Roux). diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3721a15091..dd72cd7764 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -73,7 +73,7 @@ let binder_kind_eq b1 b2 = match b1, b2 with | Generalized (ck1, b1), Generalized (ck2, b2) -> Glob_ops.binding_kind_eq ck1 ck2 && (if b1 then b2 else not b2) -| _ -> false +| (Default _ | Generalized _), _ -> false let default_binder_kind = Default Explicit diff --git a/interp/notationextern.mli b/interp/notationextern.mli index 9b947c26a1..3fd4948c59 100644 --- a/interp/notationextern.mli +++ b/interp/notationextern.mli @@ -24,6 +24,9 @@ val notation_with_optional_scope_eq : notation_with_optional_scope -> notation_w val notation_eq : notation -> notation -> bool (** Equality on [notation]. *) +val notation_binder_kind_eq : notation_binder_kind -> notation_binder_kind -> bool +(** Equality on [notation_binder_kind]. *) + val interpretation_eq : interpretation -> interpretation -> bool (** Equality on [interpretation]. *) diff --git a/parsing/extend.ml b/parsing/extend.ml index 801383e763..d27636e9be 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -37,17 +37,21 @@ type 'a constr_entry_key_gen = | ETConstr of Constrexpr.notation_entry * Notation_term.notation_binder_kind option * 'a | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) -let constr_entry_key_eq v1 v2 = match v1, v2 with +let constr_entry_key_eq_gen binder_kind_eq v1 v2 = match v1, v2 with | ETIdent, ETIdent -> true | ETName, ETName -> true | ETGlobal, ETGlobal -> true | ETBigint, ETBigint -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr (s1,bko1,_lev1), ETConstr (s2,bko2,_lev2) -> - Notationextern.notation_entry_eq s1 s2 && Option.equal (=) bko1 bko2 + Notationextern.notation_entry_eq s1 s2 && binder_kind_eq bko1 bko2 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 | (ETIdent | ETName | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false +let constr_entry_key_eq = constr_entry_key_eq_gen (Option.equal Notationextern.notation_binder_kind_eq) + +let constr_entry_key_eq_ignore_binder_kind = constr_entry_key_eq_gen (fun _ _ -> true) + (** Entries level (left-hand side of grammar rules) *) type constr_entry_key = diff --git a/parsing/extend.mli b/parsing/extend.mli index 3a7da61406..77abe962b5 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -39,6 +39,8 @@ type constr_entry_key = val constr_entry_key_eq : constr_entry_key -> constr_entry_key -> bool +val constr_entry_key_eq_ignore_binder_kind : constr_entry_key -> constr_entry_key -> bool + (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = diff --git a/test-suite/output/bug_19541.out b/test-suite/output/bug_19541.out new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test-suite/output/bug_19541.v b/test-suite/output/bug_19541.v new file mode 100644 index 0000000000..eac7193b03 --- /dev/null +++ b/test-suite/output/bug_19541.v @@ -0,0 +1,2 @@ +Reserved Notation "{[ x ]}" (at level 0, x at level 200). +Reserved Notation "{[ x | P ]}" (at level 0, x at level 200 as pattern). diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index a189096a67..da651760dd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -921,7 +921,7 @@ let check_prefix_incompatible_level ntn prec nottyps = let pref_nottyps = Notgram_ops.non_terminals_of_notation pref in let pref_nottyps = CList.firstn k pref_nottyps in let nottyps = CList.firstn k nottyps in - if not (level_eq prec pref_prec && List.for_all2 Extend.constr_entry_key_eq nottyps pref_nottyps) then + if not (level_eq prec pref_prec && List.for_all2 Extend.constr_entry_key_eq_ignore_binder_kind nottyps pref_nottyps) then warn_prefix_incompatible_level (pref, ntn, pref_prec, pref_nottyps, prec, nottyps); with Not_found | Failure _ -> ()