diff --git a/README.md b/README.md
index a2c5506d614a790d0c51218d506d570e4c87c934..ef8be0f60b9daff36558f669b4ca801b11d07e1a 100644
--- a/README.md
+++ b/README.md
@@ -36,6 +36,4 @@ the path (absolute or relative to `$HOME`) to the `exporter` directory.
 
 ### Usage
 
-Assuming PVS sources have been downloaded to `$PVSPATH`, copy
-`pvs-translation-tools` as `${PVSPATH}/translations`. Further instructions can
-be found in `pvs-translation-tools/README.md`.
+See `pvs-translation-tools/README.md`.
diff --git a/pvs-translation-tools/prelude/Makefile b/pvs-translation-tools/prelude/Makefile
index 5f44f00559b14c16986df741d6abdf4155d716a4..bedd021c4321cc18accee3e2459349dac12880f5 100644
--- a/pvs-translation-tools/prelude/Makefile
+++ b/pvs-translation-tools/prelude/Makefile
@@ -2,7 +2,7 @@ PVS2DK = ../pvs2dk.sh
 LPC    = lambdapi check
 
 THEORIES != grep -v -E '^-|\#' theories
-PVSPATH  != realpath ../..
+PVSPATH   =
 
 all: dummy ${THEORIES:C/$/.lpo/}
 
@@ -16,7 +16,7 @@ translate: dummy ${THEORIES:C/$/.lp/}
 .for th in ${THEORIES}
 ${th}.lp:
 	PVSPATH=${PVSPATH} ${PVS2DK} -f ${PVSPATH}/lib/prelude.pvs -t ${.TARGET:R} \
--o ${PVSPATH}/translations/prelude/${.TARGET} > /dev/null
+-o ${PWD}/${.TARGET} > /dev/null
 	-[ -r "${.TARGET}.patch" ] && patch < "${.TARGET}.patch"
 	-[ -r "${.TARGET}.sh" ] && sh "${.TARGET}.sh"
 .endfor
diff --git a/pvs-translation-tools/prelude/README.md b/pvs-translation-tools/prelude/README.md
index 7ca5fbb2d368c4d493ccfebdf93d6f959e807637..34da6d7dd6885b208f6df4579f41f3cb70cd409c 100644
--- a/pvs-translation-tools/prelude/README.md
+++ b/pvs-translation-tools/prelude/README.md
@@ -4,9 +4,9 @@ Prelude translation
 **Warning:** the makefile uses BSD-syntax, Linux users may use `bmake` rather than
 `make`.
 
-To translate all Prelude:
+To translate all Prelude, assuming PVS sources have been downloaded to `<PVSPATH>`
 ``` sh
-make
+make PVSPATH=<PVSPATH>
 ```
 
 Theories can be translated to lambdapi files, to translate theory "functions" of