diff options
| author | Hugo Herbelin | 2018-10-15 15:50:28 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 8f7c82b8a67a3c94073e55289996f02285c04914 (patch) | |
| tree | e219713f3408297c18da63186f40bb0b8ab0360e /doc | |
| parent | e2c4d3ad72b85f1fb1ea1a7c42aff0831eff3c30 (diff) | |
Printing priority to most recent notation in case of non-open scopes with delim.
This modifies the strategy in previous commits so that priorities are
as before in case of non-open scopes with delimiters.
Additionally, we document the rare situation of overlapping
applicative notations (maybe this is too rare and ad hoc to be worth
being documented though).
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 66fa3af052..ce79e2915e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1337,10 +1337,22 @@ Coq will use the following rules for printing priorities: - In case no abbreviation, nor lonely notation, nor notation in an explicitly open scope, nor notation in a temporarily open scope of arguments, has been found, notations in those closed scopes which - have a delimiter are considered. A notation is chosen and the - corresponding delimiter is inserted, making the corresponding scope - the most recent explicitly open scope for all subterms of the - current term. + have a delimiter are considered, giving priority to the most + recently defined (or imported) ones. The corresponding delimiter is + inserted, making the corresponding scope the most recent explicitly + open scope for all subterms of the current term. + +- As a refinement of the previous rule, in the case of applied global + references, notations in a non-opened scope with delimiter + specifically defined for this applied global reference take priority + over notations in a non-opened scope with delimiter for generic + applications. For instance, in the presence of ``Notation "f ( x + )" := (f x) (at level 10, format "f ( x )") : app_scope`` and + ``Notation "x '.+1'" := (S x) (at level 10, format "x '.+1'") : + mynat_scope.`` and both of ``app_scope`` and ``mynat_scope`` being + bound to a delimiter *and* both not opened, the latter, more + specific notation will always take precedence over the first, more + generic one. - A scope can be closed by using :cmd:`Close Scope` and its delimiter removed by using :cmd:`Undelimit Scope`. To remove automatic |