aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build8
1 files changed, 1 insertions, 7 deletions
diff --git a/Makefile.build b/Makefile.build
index eefafb0cb..28da169cf 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -69,15 +69,9 @@ TIMECMD= # is "'time -p'" to get compilation time of .v
# For instance:
# TIME="%C (%U user, %S sys, %e total, %M maxres)"
-# Since library files aren't meant to contain queries like Print Assumptions
-# nor extractions, it is safe (and quite quicker) to compile them with
-# -dont-load-proofs
-
-LOADPROOFS=-dont-load-proofs
-
COQOPTS=$(COQ_XML) $(VM)
BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
-BOOTCOQC:=$(BOOTCOQTOP) $(LOADPROOFS) -compile
+BOOTCOQC:=$(BOOTCOQTOP) -compile
# The SHOW and HIDE variables control whether make will echo complete commands
# or only abbreviated versions.