Fix handling of recursive notations with custom entries

Fixes #9532
Fixes #9490

4 files changed, 13 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/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 @