diff options
| author | Hugo Herbelin | 2017-11-25 17:19:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-29 02:40:22 +0200 |
| commit | 60daf674df3d11fa2948bbc7c9a928c09f22d099 (patch) | |
| tree | 533584dd6acd3bde940529e8d3a111eca6fcbdef /parsing/ppextend.mli | |
| parent | 33d86118c7d1bfba31008b410d81c7f45dbdf092 (diff) | |
Adding support for custom entries in notations.
- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
entries. This typically corresponds to rules of the form
'Notation "[ x ]" := x (x custom myconstr).' but also
'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
are natively recognized.
Incidentally merging ETConstr and ETConstrAsBinder.
Noticed in passing that parsing binder as custom was not done as in
constr.
Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
Diffstat (limited to 'parsing/ppextend.mli')
| -rw-r--r-- | parsing/ppextend.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli index 9f61e121a4..7eb5967a3e 100644 --- a/parsing/ppextend.mli +++ b/parsing/ppextend.mli @@ -41,7 +41,6 @@ type unparsing = type unparsing_rule = unparsing list * precedence type extra_unparsing_rules = (string * string) list - val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit val find_notation_printing_rule : notation -> unparsing_rule val find_notation_extra_printing_rules : notation -> extra_unparsing_rules |