Merge remote-tracking branch 'upstream/trunk' into trunk

1 files changed, 7 insertions, 5 deletions

diff --git a/Makefile b/Makefile
index d1fa99ccb0..66721a3ad0 100644
--- a/Makefile
+++ b/Makefile
@@ -89,8 +89,7 @@ EXISTINGMLI := $(call find, '*.mli')
 GENML4FILES:= $(ML4FILES:.ml4=.ml)
 export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
-export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
-export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
+export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
 # NB: all files in $(GENFILES) can be created initially, while
 # .ml files in $(GENML4FILES) might need some intermediate building.
@@ -116,16 +115,19 @@ NOARG: world
 .PHONY: NOARG help noconfig submake
 
 help:
-	@echo "Please use either"
+	@echo "Please use either:"
 	@echo "   ./configure"
 	@echo "   make world"
 	@echo "   make install"
 	@echo "   make clean"
 	@echo "or make archclean"
-	@echo
 	@echo "For make to be verbose, add VERBOSE=1"
+	@echo "If you want camlp5 to generate human-readable files, add READABLE_ML4=1"
 	@echo
-	@echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1"
+	@echo "Bytecode compilation is now a separate target:"
+	@echo "   make byte"
+	@echo "   make install-byte"
+	@echo "Please do not mix bytecode and native targets in the same make -j"
 
 UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?')
 ifdef UNSAVED_FILES