diff options
| author | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
| commit | dd84c113a154742dff86328ebc758097e9aac8eb (patch) | |
| tree | 67795fb720516f564d074d55d9e2aa90e3d4e7f2 /parsing/notation_gram.ml | |
| parent | 231f679965745a4d7677166e8d5f62a38ebde4e7 (diff) | |
| parent | 569ad299a8092778611fcc8ae2842151c4b276db (diff) | |
Merge PR #8115: Support for custom entries in notations (take 2, feature part)
Diffstat (limited to 'parsing/notation_gram.ml')
| -rw-r--r-- | parsing/notation_gram.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml index 346350641f..d8c08803b6 100644 --- a/parsing/notation_gram.ml +++ b/parsing/notation_gram.ml @@ -17,7 +17,8 @@ type precedence = int type parenRelation = L | E | Any | Prec of precedence type tolerability = precedence * parenRelation -type level = precedence * tolerability list * constr_entry_key list +type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list + (* first argument is InCustomEntry s for custom entries *) type grammar_constr_prod_item = | GramConstrTerminal of Tok.t |