diff options
-rw-r--r-- | intf/extend.ml | 4 | ||||
-rw-r--r-- | parsing/egramcoq.ml | 19 | ||||
-rw-r--r-- | vernac/metasyntax.ml | 4 |
3 files changed, 15 insertions, 12 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index 5552bed55..e4d014a09 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,8 @@ type production_level = | NextLevel | NumLevel of int +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list + type ('lev,'pos) constr_entry_key_gen = | ETName | ETReference | ETBigint | ETBinder of bool @@ -36,7 +38,7 @@ type ('lev,'pos) constr_entry_key_gen = | ETPattern | ETOther of string * string | ETConstrList of ('lev * 'pos) * Tok.t list - | ETBinderList of bool * Tok.t list + | ETBinderList of binder_entry_kind (** Entries level (left-hand-side of grammar rules) *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ea6266dd4..16124c26c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -232,8 +232,8 @@ type (_, _) entry = | TTBinder : ('self, local_binder_expr list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry -| TTBinderListT : ('self, local_binder_expr list) entry -| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry +| TTOpenBinderList : ('self, local_binder_expr list) entry +| TTClosedBinderList : Tok.t list -> ('self, local_binder_expr list list) entry type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry @@ -289,11 +289,11 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) symbol = fun as Alist1 (symbol_of_target typ' assoc from forpat) | TTConstrList (typ', tkl, forpat) -> Alist1sep (symbol_of_target typ' assoc from forpat, make_sep_rules tkl) -| TTBinderListF [] -> Alist1 (Aentry Constr.binder) -| TTBinderListF tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) +| TTClosedBinderList [] -> Alist1 (Aentry Constr.binder) +| TTClosedBinderList tkl -> Alist1sep (Aentry Constr.binder, make_sep_rules tkl) | TTName -> Aentry Prim.name | TTBinder -> Aentry Constr.binder -| TTBinderListT -> Aentry Constr.open_binders +| TTOpenBinderList -> Aentry Constr.open_binders | TTBigint -> Aentry Prim.bigint | TTReference -> Aentry Constr.global @@ -307,9 +307,8 @@ let interp_entry forpat e = match e with | ETPattern -> assert false (** not used *) | ETOther _ -> assert false (** not used *) | ETConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) -| ETBinderList (true, []) -> TTAny TTBinderListT -| ETBinderList (true, _) -> assert false -| ETBinderList (false, tkl) -> TTAny (TTBinderListF tkl) +| ETBinderList ETBinderOpen -> TTAny TTOpenBinderList +| ETBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) let constr_expr_of_name (loc,na) = CAst.make ?loc @@ match na with | Anonymous -> CHole (None,Misctypes.IntroAnonymous,None) @@ -336,8 +335,8 @@ match e with | ForPattern -> push_constr subst (cases_pattern_expr_of_name v) end | TTBinder -> { subst with binders = (v, true) :: subst.binders } -| TTBinderListT -> { subst with binders = (v, true) :: subst.binders } -| TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders } +| TTOpenBinderList -> { subst with binders = (v, true) :: subst.binders } +| TTClosedBinderList _ -> { subst with binders = (List.flatten v, false) :: subst.binders } | TTBigint -> begin match forpat with | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (v,true))) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c295434d0..bb4db1322 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -656,8 +656,10 @@ let make_production etyps symbols = let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in expand_list_rule typ tkl x 1 p (aux l') | ETBinder o -> + check_open_binder o sl x; + let typ = if o then (assert (tkl = []); ETBinderOpen) else ETBinderClosed tkl in distribute - [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] (aux l) + [GramConstrNonTerminal (ETBinderList typ, Some x)] (aux l) | _ -> user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in let prods = aux symbols in |