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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/egramcoq.ml | 6 | ||||
| -rw-r--r-- | parsing/egramcoq.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index ec422c58d..1b38a013c 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -464,7 +464,7 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () -let extend_constr_notation (_, ng) state = +let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> default_constr_levels | Some lev -> lev @@ -476,7 +476,7 @@ let extend_constr_notation (_, ng) state = let state = GramState.set state constr_levels levels in (r @ r', state) -let constr_grammar : (Notation.level * notation_grammar) grammar_command = +let constr_grammar : one_notation_grammar grammar_command = create_grammar_command "Notation" extend_constr_notation -let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn) +let extend_constr_grammar ntn = extend_grammar_command constr_grammar ntn diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 248de3348..8e0469275 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -13,5 +13,5 @@ (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit +val extend_constr_grammar : Notation_term.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) |