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/sphinx/proof-engine/ltac2.rst | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc/sphinx/proof-engine')

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