From 5efdfe979fd316372c59d9406fa7ade46aa6814a Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 25 Oct 2019 13:13:43 +0200
Subject: fix coq_makefile and doc for vos support.

---
 doc/sphinx/practical-tools/coq-commands.rst | 2 +-
 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 $<
-- 
cgit v1.2.3