Merge PR #11311: Fix handling of recursive notations with custom entries

Reviewed-by: herbelin

6 files changed, 34 insertions, 8 deletions

diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst
new file mode 100644
index 0000000000..ae9888512d
--- /dev/null
+++ b/doc/changelog/03-notations/11311-custom-entries-recursive.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Recursive notations with custom entries were incorrectly parsing `constr`
+  instead of custom grammars (`#11311 <https://github.com/coq/coq/pull/11311>`_
+  by Maxime Dénès, fixes `#9532 <https://github.com/coq/coq/pull/9532>`_,
+  `#9490 <https://github.com/coq/coq/pull/9490>`_).
diff --git a/parsing/extend.ml b/parsing/extend.ml
index ed6ebe5aed..dcdaa25c33 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -54,7 +54,7 @@ type constr_prod_entry_key =
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
   | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *)
   | ETProdPattern of int  (* Parsed as pattern as a binder (as subpart of a constr) *)
-  | ETProdConstrList of (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr *)
+  | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *)
   | ETProdBinderList of binder_entry_kind  (* Parsed as non-empty list of local binders *)
 
 (** {5 AST for user-provided entries} *)
diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/bug_9490.v
new file mode 100644
index 0000000000..a5def40c49
--- /dev/null
+++ b/test-suite/bugs/bug_9490.v
@@ -0,0 +1,9 @@
+Declare Custom Entry with_pattern.
+Declare Custom Entry M_branch.
+Notation "'with' | p1 | .. | pn 'end'" :=
+  (cons p1 (.. (cons pn nil) ..))
+  (in custom with_pattern at level 91, p1 custom M_branch at level 202, pn custom M_branch at level 202).
+Notation "'bla'" := I (in custom M_branch at level 202).
+Notation "'[use_with'  l  ]" := (l) (at level 0, l custom with_pattern at level 91).
+Check [use_with with | bla end].
+Check [use_with with | bla | bla end].
diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/bug_9532.v
new file mode 100644
index 0000000000..d198d45f2f
--- /dev/null
+++ b/test-suite/bugs/bug_9532.v
@@ -0,0 +1,12 @@
+Declare Custom Entry atom.
+Notation "1" := tt (in custom atom).
+Notation "atom:( s )" := s (s custom atom).
+
+Declare Custom Entry expr.
+Notation "expr:( s )" := s (s custom expr).
+Notation "( x , y , .. , z )" :=  (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..))
+  (in custom expr at level 0, x custom atom, y custom atom, z custom atom).
+
+Check atom:(1).
+Check expr:((1,1)).
+Check expr:((1,1,1)).
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e02f94629c..b65a126f55 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -247,7 +247,7 @@ type (_, _) entry =
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, string) entry
 | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
+| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
 | TTPattern : int -> ('self, cases_pattern_expr) entry
 | TTOpenBinderList : ('self, local_binder_expr list) entry
 | TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry
@@ -347,12 +347,12 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym
 
 let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
 | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
-| TTConstrList (typ', [], forpat) ->
-  begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+| TTConstrList (s, typ', [], forpat) ->
+  begin match symbol_of_target s typ' assoc from forpat with
   | MayRecNo s -> MayRecNo (Alist1 s)
   | MayRecMay s -> MayRecMay (Alist1 s) end
-| TTConstrList (typ', tkl, forpat) ->
-  begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+| TTConstrList (s, typ', tkl, forpat) ->
+  begin match symbol_of_target s typ' assoc from forpat with
   | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
   | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
 | TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
@@ -369,7 +369,7 @@ let interp_entry forpat e = match e with
 | ETProdBigint -> TTAny TTBigint
 | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
 | ETProdPattern p -> TTAny (TTPattern p)
-| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
 | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
 | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e23522da9e..35681aed13 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -611,7 +611,7 @@ let expand_list_rule s typ tkl x n p ll =
   else if Int.equal i (p+n) then
     let hds =
       GramConstrListMark (p+n,true,p) :: hds
-      @	[GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in
+      @	[GramConstrNonTerminal (ETProdConstrList (s, typ,tkl), Some x)] in
     distribute hds ll
   else
     distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @