diff options
| author | charguer | 2019-10-25 13:13:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-01 12:16:49 +0100 |
| commit | 5efdfe979fd316372c59d9406fa7ade46aa6814a (patch) | |
| tree | 02945b5124ae1b02a006c15094eb3c371e8e64cb | |
| parent | fb6afb4a7256b33725660668738bc17c84ae94f5 (diff) | |
fix coq_makefile and doc for vos support.
| -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 $< |