From b60906cc3ee3f994babf9cceff2971bd03485f2f Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 22 Jan 2018 12:45:49 -0800
Subject: Change references to CAMLP4 to CAMLP5 to be more accurate since we no
 longer use camlp4.

---
 dev/doc/build-system.txt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/doc/build-system.txt')

diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 873adc1b22..1c4fd2eba4 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This
 enables partial recalculation of dependencies (only the dependencies
 of changed files are recomputed).
 
-If you add a dependency to a Coq camlp4 extension (grammar.cma or
+If you add a dependency to a Coq camlp5 extension (grammar.cma or
 q_constr.cmo), then see sections ".ml4 files" and "new files".
 
 Cleaning Targets
@@ -127,7 +127,7 @@ of a grammar extension via a line of the form:
 
 The use of (*i camlp4use: ... i*) to mention uses of standard
 extension such as IFDEF has also been discontinued, the Makefile now
-always calls camlp4 with pa_macros.cmo and a few others by default.
+always calls camlp5 with pa_macros.cmo and a few others by default.
 
 For debugging a Coq grammar extension, it could be interesting
 to use the READABLE_ML4=1 option, otherwise the generated .ml are
-- 
cgit v1.2.3