diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-24 20:04:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:18:49 +0200 |
| commit | f442efebd8354b233827e4991a80d27082c772e1 (patch) | |
| tree | dfdc1a38defaa4f2e7ca413aaca883f5c2b728fa /intf | |
| parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) | |
A little reorganization of notations + a fix to #5608.
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/notation_term.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index cee96040b..084a1042c 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -88,11 +88,12 @@ type grammar_constr_prod_item = concat with last parsed list when true; additionally release the p last items as if they were parsed autonomously *) -type notation_grammar = { +type one_notation_grammar = { notgram_level : int; notgram_assoc : Extend.gram_assoc option; notgram_notation : Constrexpr.notation; notgram_prods : grammar_constr_prod_item list list; notgram_typs : notation_var_internalization_type list; - notgram_onlyprinting : bool; } + +type notation_grammar = (* onlyprinting *) bool * one_notation_grammar list |