From 724966f56caa66a5ddc9a992cf870ebc2efae004 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 7 Sep 2020 11:53:49 +0200
Subject: [refman] Rename int to integer

---
 doc/sphinx/user-extensions/syntax-extensions.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8474d0287f..d31ec51d52 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1887,7 +1887,7 @@ Tactic notations allow customizing the syntax of tactics.
         - :tacn:`refine`
 
       * - ``integer``
-        - :token:`int`
+        - :token:`integer`
         - an integer
         -
 
-- 
cgit v1.2.3