diff options
| author | Maxime Dénès | 2019-12-19 12:45:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-12-20 13:27:13 +0100 |
| commit | 7149fef354d55f4b5012eac7efa15b4e7bac3d38 (patch) | |
| tree | ab27bfa6035490d65205702854d34dd16411c029 /vernac/metasyntax.ml | |
| parent | 5c667d56cd0a441f787019aef44bf18bec9c7b20 (diff) | |
Fix handling of recursive notations with custom entries
Fixes #9532
Fixes #9490
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 @ |