aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-31 17:01:17 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-31 17:01:17 +0200
commitce4c3ddec6c91dc277c922aaac58395c92941710 (patch)
tree9414d87506c0c075aed8caa53199c30bb47f2890 /Makefile.common
parent505eb0f0dae9b8a6ac810070d60916b67942b305 (diff)
Improve the table of content of the reference manual.
Also remove AsyncProofs.tex from the list of preprocessed files, as it is doubtful it will ever contains Coq scripts.
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common
index 07df8bb15..de26eeb9b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -127,13 +127,14 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
- Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \
+ Setoid.v.tex Classes.v.tex Universes.v.tex \
Misc.v.tex)
REFMANTEXFILES:=$(addprefix doc/refman/, \
headers.sty Reference-Manual.tex \
RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
- RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \
+ RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
+ AsyncProofs.tex ) \
$(REFMANCOQTEXFILES) \
REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps