diff options
| author | Pierre-Marie Pédrot | 2019-03-31 23:07:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-31 23:07:48 +0200 |
| commit | 5dd3c18f4e50eef53ae4413b7b80951f17edad5f (patch) | |
| tree | 0a104d6afc109b7b89c8997d1afb3bc9f1e89dc3 /parsing/extend.ml | |
| parent | cb502e44aac8328ffd6c37429e050a01f72b2c53 (diff) | |
| parent | f832476404a29d7791c1a6d7970988d3b2e3ad9e (diff) | |
Merge PR #9733: [lexer] keyword protected quotation token for arbitrary text
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 9b5537d7f6..ff879dd1c2 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -44,7 +44,7 @@ type simple_constr_prod_entry_key = (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) -type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.t list +type binder_entry_kind = ETBinderOpen | ETBinderClosed of Tok.pattern list type binder_target = ForBinder | ForTerm @@ -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) * Tok.t list (* Parsed as non-empty list of constr *) + | ETProdConstrList of (production_level * production_position) * Tok.pattern list (* Parsed as non-empty list of constr *) | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) (** {5 AST for user-provided entries} *) @@ -80,7 +80,7 @@ type ('a,'b,'c) ty_user_symbol = (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = -| Atoken : Tok.t -> ('self, string) symbol +| Atoken : Tok.pattern -> ('self, string) symbol | Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol | Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol | Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol |