diff options
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9da565aa3c..d8325287cc 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -309,7 +309,7 @@ working state for editing interactively the file ``foo.v``. **Typical compilation of a set of file using a build system.** Assume a file ``foo.v`` that depends on two files ``f1.v`` and ``f2.v``. The -command ``make foo.requires_vos`` will compile ``f1.v`` and ``f2.v`` using +command ``make foo.required_vos`` will compile ``f1.v`` and ``f2.v`` using the option ``-vos`` to skip the proofs, producing ``f1.vos`` and ``f2.vos``. At this point, one is ready to work interactively on the file ``foo.v``, even though it was never needed to compile the proofs involved in the files ``f1.v`` diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 1cceed79a4..b8930997a4 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -676,11 +676,11 @@ $(VFILES:.v=.vio): %.vio: %.v $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< - $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vok): %.vok: %.v $(SHOW)COQC -vok $< - $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing $(SHOW)PYTHON TIMING-DIFF $< |