diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 4 | ||||
| -rw-r--r-- | dev/core.dbg | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.dev.txt | 2 | ||||
| -rw-r--r-- | dev/doc/build-system.txt | 4 | ||||
| -rw-r--r-- | dev/doc/coq-src-description.txt | 2 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 6 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
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 ] |