From 6eb4dbf6ba77ae7e9087832ea1e27426b515a8e8 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 10 Feb 2020 18:54:55 +0100 Subject: Custom entries: accept that no level is mentioned for a subentry. If it is for an internal non-terminal then: - if for a subentry different from constr, it refers to the head of the subentry - if in constr, it is 200 by convention If it is on the border of a rule, then: - if it is in a subentry different from the entry it lives, it refers to the head of the subentry (or 200 by convention if in constr) - if it is in the same entry, the rule for associativity tells if a SELF, a NEXT, or (if on the right) a LEVEL --- doc/sphinx/user-extensions/syntax-extensions.rst | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..a8d5ac610f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to -- cgit v1.2.3 From acde8140bd51be112be33ae07db68b2f3b93302c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Jan 2020 20:02:38 +0100 Subject: Adding change log. --- .../11530-master+fix11331-custom-entries-precedence.rst | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst (limited to 'doc') diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst new file mode 100644 index 0000000000..b105928b22 --- /dev/null +++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Bugs in dealing with precedences of notations in custom entries + (`#11530 `_, + by Hugo Herbelin, fixing in particular + `#9517 `_, + `#9519 `_, + `#9521 `_, + `#11331 `_). -- cgit v1.2.3