From 7149fef354d55f4b5012eac7efa15b4e7bac3d38 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 19 Dec 2019 12:45:28 +0100
Subject: Fix handling of recursive notations with custom entries

Fixes #9532
Fixes #9490
---
 parsing/extend.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

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} *)
-- 
cgit v1.2.3