From ed9bc81551eb8cf9e51d3824add3fa0b5b6c88a9 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 18 Mar 2011 11:03:05 +0000
Subject: Makefile.build: compile the stdlib with -dont-load-proofs by default

 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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13918 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index d141528420..d97b8e0975 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -69,7 +69,13 @@ TIMECMD=	# is "'time -p'" to get compilation time of .v
 # For instance:
 # TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-COQOPTS=$(COQ_XML) $(VM)
+# 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) $(LOADPROOFS)
 BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
-- 
cgit v1.2.3