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 /vernac/metasyntax.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 'vernac/metasyntax.mli')
| -rw-r--r-- | vernac/metasyntax.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index f6de75b079..045b8fa05c 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -60,3 +60,5 @@ val pr_grammar : string -> Pp.t val check_infix_modifiers : syntax_modifier list -> unit val with_syntax_protection : ('a -> 'b) -> 'a -> 'b + +val declare_custom_entry : string -> unit |