Merge PR #19653: Fix #19451 (spurious incompatible-prefix warning when using "as pattern")

Reviewed-by: herbelin
Ack-by: ppedrot
Co-authored-by: herbelin <[email protected]>

Author: coqbot-app[bot]

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 <https://github.com/coq/coq/pull/19653>`_,
+  fixes `#19541 <https://github.com/coq/coq/issues/19541>`_,
+  by Pierre Roux).

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
 

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]. *)
 

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 =

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 =

test-suite/output/bug_19541.out

@@ -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).

test-suite/output/bug_19541.v

@@ -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 _ -> ()