From a7f56cb5799bc830285f4acf96678486a5929172 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 29 Feb 2020 12:27:51 -0800
Subject: Convert syntax extensions chapter to prodn

---
 doc/sphinx/practical-tools/coqide.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/sphinx/practical-tools')

diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index a69521c278..0f255e4e64 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -219,7 +219,7 @@ Displaying Unicode symbols
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 You just need to define suitable notations as described in the chapter
-:ref:`syntaxextensionsandinterpretationscopes`. For example, to use the
+:ref:`syntaxextensionsandnotationscopes`. For example, to use the
 mathematical symbols ∀ and ∃, you may define:
 
 .. coqtop:: in
-- 
cgit v1.2.3