aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-05 21:57:15 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-08-05 21:57:15 +0200
commit2bb05717bde540332aa814a59da3745f2097dedf (patch)
tree86f5753cb84e300e13e9bda8fb8c3835bd66b41a /Makefile.common
parente76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (diff)
parentdda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 (diff)
Merge branch 'v8.5'
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 15ac13ff1..a28ca1dfc 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