diff options
| author | letouzey | 2011-03-18 11:03:05 +0000 |
|---|---|---|
| committer | letouzey | 2011-03-18 11:03:05 +0000 |
| commit | ed9bc81551eb8cf9e51d3824add3fa0b5b6c88a9 (patch) | |
| tree | 34ca0faabfda229c2b0c8aca2d57c1698978eb60 | |
| parent | 404c0f9c6b189c4273a9bc1698765eaa6a664389 (diff) | |
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
| -rw-r--r-- | Makefile.build | 8 |
1 files changed, 7 insertions, 1 deletions
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 |