From acc7acfa0e8015b5785cb0f2d01acca2448e8197 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 31 Jul 2018 22:34:02 -0400
Subject: Camlp{4 => 5}

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

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 39f845d81c..37394386e6 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1457,7 +1457,7 @@ tactic language. Tactic notations obey the following syntax:
 
 .. [#no_associativity] Coq accepts notations declared as ``no
    associativity`` but the parser on which Coq is built, namely
-   Camlp4, currently does not implement ``no associativity`` and
+   Camlp5, currently does not implement ``no associativity`` and
    replaces it with ``left associativity``; hence it is the same for
    Coq: ``no associativity`` is in fact ``left associativity``, for
    the purposes of parsing
-- 
cgit v1.2.3