Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use camlp4

8 files changed, 11 insertions, 12 deletions

diff --git a/dev/base_include b/dev/base_include
index 472c0c605..320d366aa 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -19,7 +19,6 @@
 #directory "stm";;
 #directory "vernac";;
 
-#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
 
 #use "top_printers.ml";;
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index c46767821..d8cde39f8 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -794,8 +794,8 @@ function make_ocaml {
     # TODO: this might not work if PREFIX contains spaces
     sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
     
-    # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder
-    # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path:
+    # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder
+    # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
     # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
     # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
     # So we put an explicit path in there
diff --git a/dev/core.dbg b/dev/core.dbg
index 00a4355a4..57c136900 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -1,4 +1,4 @@
-source camlp4.dbg
+source camlp5.dbg
 load_printer threads.cma
 load_printer str.cma
 load_printer clib.cma
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index f3fc13e96..abba13428 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -46,7 +46,7 @@ see build-system.txt .
 .ml4 files
 ----------
 
-.ml4 are converted to .ml by camlp4. By default, they are produced
+.ml4 are converted to .ml by camlp5. By default, they are produced
 in the binary ast format understood by ocamlc/ocamlopt/ocamldep.
 Pros:
  - faster than parsing clear-text source file.
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index 873adc1b2..1c4fd2eba 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
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 2dbd132da..b3d49b7e5 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -25,7 +25,7 @@ intf :
 
 grammar :
 
- Camlp4 syntax extensions. The file grammar/grammar.cma is used
+ Camlp5 syntax extensions. The file grammar/grammar.cma is used
  to pre-process .ml4 files containing EXTEND constructions,
  either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND.
  This grammar.cma incorporates many files from other directories
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 3cbccab44..f3e60edea 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -3,19 +3,19 @@
 # Wrapper around ocamldebug for Coq
 
 # This file is to be launched via the generated script ocamldebug-coq,
-# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP
+# which will set the env variables $OCAMLDEBUG, $CAMLP5LIB, $COQTOP
 # Anyway, just in case someone tries to use this script directly,
 # here are some reasonable default values
 
 [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug
-[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5
+[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5
 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
 [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
 exec $OCAMLDEBUG \
-	-I $CAMLP4LIB -I +threads \
+	-I $CAMLP5LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
 	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index af38ce4b8..f99e2593d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -485,7 +485,7 @@ let in_current_context f c =
   let (evmap,sign) = Pfedit.get_current_context () in
   f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
-(* We expand the result of preprocessing to be independent of camlp4
+(* We expand the result of preprocessing to be independent of camlp5
 
 VERNAC COMMAND EXTEND PrintPureConstr
 | [ "PrintPureConstr" constr(c) ] -> [ in_current_context print_pure_constr c ]