diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-25 17:09:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
| commit | 8f93f9a2df6e17386f46f79b2a7eda4104d0a94e (patch) | |
| tree | 77c1c1fdc54a7c96d197c71caa2ab75fc3041928 /intf | |
| parent | 69822345c198aa6bf51354f6b84c7fd5d401bc9c (diff) | |
Notations: A step in cleaning constr_entry_key.
- Avoid dummy use of unit
- Do not decide as early as parsing the default level for pattern
- Prepare to further extensions
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/intf/extend.ml b/intf/extend.ml index 5258ef56b..813ed6dc6 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -31,24 +31,24 @@ type production_level = (** User-level types used to tell how to parse or interpret of the non-terminal *) -type ('lev,'pos) constr_entry_key_gen = +type 'a constr_entry_key_gen = | ETName | ETReference | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) - | ETConstr of ('lev * 'pos) - | ETPattern of int + | ETConstr of 'a + | ETPattern of int option | ETOther of string * string (** Entries level (left-hand side of grammar rules) *) type constr_entry_key = - (production_level,production_position) constr_entry_key_gen + (production_level * production_position) constr_entry_key_gen (** Entries used in productions, vernac side (e.g. "x bigint" or "x ident") *) type simple_constr_prod_entry_key = - (production_level,unit) constr_entry_key_gen + production_level option constr_entry_key_gen (** Entries used in productions (in right-hand-side of grammar rules), to parse non-terminals *) |