Change references to CAMLP4 to CAMLP5 to be more accurate since we no

longer use camlp4.

.gitignore

@@ -55,7 +55,7 @@ config/Makefile
 config/coq_config.ml
 config/Info-*.plist
 dev/ocamldebug-coq
-dev/camlp4.dbg
+dev/camlp5.dbg
 plugins/micromega/csdpcert
 plugins/micromega/.micromega.ml.generated
 kernel/byterun/dllcoqrun.so

Makefile

@@ -266,7 +266,7 @@ cacheclean:
 	find theories plugins test-suite -name '.*.aux' -delete
 
 cleanconfig:
-	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist
+	rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
 
 distclean: clean cleanconfig cacheclean timingclean
 

Makefile.build

@@ -196,7 +196,7 @@ COQOPTS=$(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
 LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS))
-MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
+MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP5LIB)
 
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
@@ -240,8 +240,8 @@ endef
 
 # Camlp5 settings
 
-CAMLP4DEPS:=grammar/grammar.cma
-CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
+CAMLP5DEPS:=grammar/grammar.cma
+CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
 
 PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo)
 
@@ -345,14 +345,14 @@ grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \
 ## Ocaml compiler with the right options and -I for grammar
 
 GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \
- -I $(MYCAMLP4LIB) -I grammar
+ -I $(MYCAMLP5LIB) -I grammar
 
 ## Specific rules for grammar.cma
 
 grammar/grammar.cma : $(GRAMCMO)
 	$(SHOW)'Testing $@'
 	@touch grammar/test.mlp
-	$(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
+	$(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test
 	@rm -f grammar/test.* grammar/test
 	$(SHOW)'OCAMLC -a $@'
 	$(HIDE)$(GRAMC) $^ -linkall -a -o $@
@@ -361,7 +361,7 @@ grammar/grammar.cma : $(GRAMCMO)
 
 COMPATCMO:=
 GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION)
-GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl
+GRAMPP:=$(CAMLP5O) -I $(MYCAMLP5LIB) $(GRAMP4USE) $(CAMLP5COMPAT) -impl
 
 ## Rules for standard .mlp and .mli files in grammar/
 
@@ -684,10 +684,10 @@ plugins/%.cmx: plugins/%.ml
 	$(SHOW)'OCAMLLEX  $<'
 	$(HIDE)$(OCAMLLEX) -o $@ "$*.mll"
 
-%.ml: %.ml4 $(CAMLP4DEPS)
+%.ml: %.ml4 $(CAMLP5DEPS)
 	$(SHOW)'CAMLP5O   $<'
-	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \
-	  $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@
+	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \
+	  $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@
 
 
 ###########################################################################

Makefile.dev

@@ -18,9 +18,9 @@
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo
 
 devel: printers
-printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg
+printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg
 
-dev/camlp4.dbg:
+dev/camlp5.dbg:
 	echo "load_printer gramlib.cma" > $@
 
 ############

Makefile.ide

@@ -106,9 +106,9 @@ $(COQIDEBYTE): $(LINKIDE)
 	$(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \
 	        lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^
 
-ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
-	$(SHOW)'CAMLP4O   $<'
-	$(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@
+ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here
+	$(SHOW)'CAMLP5O   $<'
+	$(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@
 
 
 ide/%.cmi: ide/%.mli

checker/include

@@ -13,7 +13,6 @@
 #directory "kernel";;
 #directory "checker";;
 #directory "+threads";;
-#directory "+camlp4";;
 #directory "+camlp5";;
 
 #load "unix.cma";;

config/coq_config.mli

@@ -28,11 +28,10 @@ val ocamllex : string
 val camlbin : string    (* base directory of OCaml binaries *)
 val camllib : string    (* for Dynlink *)
 
-val camlp4 : string     (* exact name of camlp4: either "camlp4" ou "camlp5" *)
-val camlp4o : string    (* name of the camlp4o/camlp5o executable *)
-val camlp4bin : string  (* base directory for Camlp4/5 binaries *)
-val camlp4lib : string  (* where is the library of Camlp4 *)
-val camlp4compat : string (* compatibility argument to camlp4/5 *)
+val camlp5o : string    (* name of the camlp5o executable *)
+val camlp5bin : string  (* base directory for camlp5 binaries *)
+val camlp5lib : string  (* where is the library of camlp5 *)
+val camlp5compat : string (* compatibility argument to camlp5 *)
 
 val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *)
 val cflags : string     (* arguments passed to gcc *)

configure.ml

@@ -193,7 +193,7 @@ let select_command msg candidates =
   in search candidates
 
 (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it
-    a quoted path to camlpXo via -pp.  So we only quote camlpXo on not
+    a quoted path to camlp5o via -pp.  So we only quote camlp5o on not
     Windows, and warn on Windows if the path contains spaces *)
 let contains_suspicious_characters str =
   List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t']
@@ -487,7 +487,7 @@ let camlbin, caml_version, camllib, findlib_version =
       then reset_caml_top camlexec (camlbin / "ocaml") in
     camlbin, caml_version, camllib, findlib_version
 
-let camlp4compat = "-loc loc"
+let camlp5compat = "-loc loc"
 
 (** Caml version as a list of string, e.g. ["4";"00";"1"] *)
 
@@ -570,9 +570,9 @@ let caml_flags =
 let coq_caml_flags =
   coq_warn_error
 
-(** * CamlpX configuration *)
+(** * Camlp5 configuration *)
 
-(* Convention: we use camldir as a prioritary location for camlpX, if given *)
+(* Convention: we use camldir as a prioritary location for camlp5, if given *)
 (* i.e., in the case of camlp5, we search for a copy of camlp5o which *)
 (* answers the right camlp5 lib dir *)
 
@@ -588,7 +588,7 @@ let which_camlp5o_for camlp5lib =
   if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else
   die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib)
 
-let which_camlpX base =
+let which_camlp5 base =
   let file = Filename.concat camlbin base in
   if is_executable file then file else which base
 
@@ -609,7 +609,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
       in die msg
   | None ->
     try
-      let camlp5o = which_camlpX "camlp5o" in
+      let camlp5o = which_camlp5 "camlp5o" in
       let dir,_ = tryrun camlp5o ["-where"] in
       dir, camlp5o
     with Not_found ->
@@ -623,23 +623,22 @@ let check_camlp5_version camlp5o =
     printf "You have Camlp5 %s. Good!\n" version; version
   | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
 
-let config_camlpX () =
+let config_camlp5 () =
     let camlp5mod = "gramlib" in
     let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in
     let camlp5_version = check_camlp5_version camlp5o in
-    "camlp5", "Camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
+    camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
 
-let camlpX, capitalized_camlpX, camlpXo,
-    camlpXbindir, fullcamlpXlibdir,
-    camlpXmod, camlpX_version = config_camlpX ()
+let camlp5o, camlp5bindir, fullcamlp5libdir,
+    camlp5mod, camlp5_version = config_camlp5 ()
 
 let shorten_camllib s =
   if starts_with s (camllib^"/") then
     let l = String.length camllib + 1 in
     "+" ^ String.sub s l (String.length s - l)
   else s
 
-let camlpXlibdir = shorten_camllib fullcamlpXlibdir
+let camlp5libdir = shorten_camllib fullcamlp5libdir
 
 (** * Native compiler *)
 
@@ -649,8 +648,8 @@ let msg_byteonly () =
 let msg_no_ocamlopt () =
   printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly ()
 
-let msg_no_camlpX_cmxa () =
-  printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly ()
+let msg_no_camlp5_cmxa () =
+  printf "Cannot find the native-code library of camlp5.\n"; msg_byteonly ()
 
 let msg_no_dynlink_cmxa () =
   printf "Cannot find native-code dynlink library.\n"; msg_byteonly ();
@@ -662,8 +661,8 @@ let check_native () =
   let () = if !Prefs.byteonly then raise Not_found in
   let version, _ = tryrun camlexec.find ["opt";"-version"] in
   if version = "" then let () = msg_no_ocamlopt () in raise Not_found
-  else if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa"))
-  then let () = msg_no_camlpX_cmxa () in raise Not_found
+  else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa"))
+  then let () = msg_no_camlp5_cmxa () in raise Not_found
   else if fst (tryrun camlexec.find ["query";"dynlink"]) = ""
   then let () = msg_no_dynlink_cmxa () in raise Not_found
   else
@@ -1015,9 +1014,9 @@ let print_summary () =
   pr "  OCaml binaries in           : %s\n" (esc camlbin);
   pr "  OCaml library in            : %s\n" (esc camllib);
   pr "  OCaml flambda flags         : %s\n" (String.concat " " !Prefs.flambda_flags);
-  pr "  %s version              : %s\n"     capitalized_camlpX camlpX_version;
-  pr "  %s binaries in          : %s\n"     capitalized_camlpX (esc camlpXbindir);
-  pr "  %s library in           : %s\n"     capitalized_camlpX (esc camlpXlibdir);
+  pr "  Camlp5 version              : %s\n" camlp5_version;
+  pr "  Camlp5 binaries in          : %s\n" (esc camlp5bindir);
+  pr "  Camlp5 library in           : %s\n" (esc camlp5libdir);
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
@@ -1057,7 +1056,7 @@ let write_dbg_wrapper f =
   pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n";
   pr "export COQTOP=%S\n" coqtop;
   pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug");
-  pr "CAMLP4LIB=%S\n\n" camlpXlibdir;
+  pr "CAMLP5LIB=%S\n\n" camlp5libdir;
   pr ". $COQTOP/dev/ocamldebug-coq.run\n";
   close_out o;
   Unix.chmod f 0o555
@@ -1095,11 +1094,10 @@ let write_configml f =
   pr_s "ocamllex" camlexec.lex;
   pr_s "camlbin" camlbin;
   pr_s "camllib" camllib;
-  pr_s "camlp4" camlpX;
-  pr_s "camlp4o" camlpXo;
-  pr_s "camlp4bin" camlpXbindir;
-  pr_s "camlp4lib" camlpXlibdir;
-  pr_s "camlp4compat" camlp4compat;
+  pr_s "camlp5o" camlp5o;
+  pr_s "camlp5bin" camlp5bindir;
+  pr_s "camlp5lib" camlp5libdir;
+  pr_s "camlp5compat" camlp5compat;
   pr_s "cflags" cflags;
   pr_s "caml_flags" caml_flags;
   pr_s "best" best_compiler;
@@ -1220,12 +1218,11 @@ let write_makefile f =
   pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag;
   pr "# Compilation profile flag\n";
   pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag;
-  pr "# Camlp4 : flavor, binaries, libraries ...\n";
-  pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n";
-  pr "CAMLP4=%s\n" camlpX;
-  pr "CAMLP4O=%s\n" (win_aware_quote_executable camlpXo);
-  pr "CAMLP4COMPAT=%s\n" camlp4compat;
-  pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir;
+  pr "# Camlp5 : flavor, binaries, libraries ...\n";
+  pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n";
+  pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o);
+  pr "CAMLP5COMPAT=%s\n" camlp5compat;
+  pr "MYCAMLP5LIB=%S\n\n" camlp5libdir;
   pr "# Your architecture\n";
   pr "# Can be obtain by UNIX command arch\n";
   pr "ARCH=%s\n" arch;

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";;

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

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

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.

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

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

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 \

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 ]

ide/minilib.ml

@@ -20,7 +20,7 @@ type level = [
   | `FATAL ]
 
 (** Some excerpt of Util and similar files to avoid loading the whole
-    module and its dependencies (and hence Compat and Camlp4) *)
+    module and its dependencies (and hence Compat and Camlp5) *)
 
 let debug = ref false
 

ide/minilib.mli

@@ -7,7 +7,7 @@
 (***********************************************************************)
 
 (** Some excerpts of Util and similar files to avoid depending on them
-    and hence on Compat and Camlp4 *)
+    and hence on Compat and Camlp5 *)
 
 val print_list : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit