From f6e393dae62afbb659eab64a530c0cf39403c495 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 8 Apr 2021 15:39:56 +0200 Subject: Properly pass the Ltac2 notation level to the gramlib API. For some reason I was confusing the position and the level in the previous version of the code. Fixes #11866: Ltac2 Notations do not respect precedence. --- doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst | 5 +++++ doc/sphinx/proof-engine/ltac2.rst | 4 ++++ 2 files changed, 9 insertions(+) create mode 100644 doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst (limited to 'doc') diff --git a/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst new file mode 100644 index 0000000000..41bc3329c1 --- /dev/null +++ b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Ltac2 notations now correctly take into account their assigned level + (`#14094 `_, + fixes `#11866 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 25ac72069b..52cf565998 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1251,6 +1251,10 @@ Notations This command supports the :attr:`deprecated` attribute. + .. exn:: Notation levels must range between 0 and 6. + + The level of a notation must be an integer between 0 and 6 inclusive. + Abbreviations ~~~~~~~~~~~~~ -- cgit v1.2.3