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 | |
| parent | 5c667d56cd0a441f787019aef44bf18bec9c7b20 (diff) | |
Fix handling of recursive notations with custom entries
Fixes #9532
Fixes #9490
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 12 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
2 files changed, 7 insertions, 7 deletions
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 @ |