diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-05 21:57:15 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-05 21:57:15 +0200 |
commit | 2bb05717bde540332aa814a59da3745f2097dedf (patch) | |
tree | 86f5753cb84e300e13e9bda8fb8c3835bd66b41a /Makefile.common | |
parent | e76ab0ec81040cbe99f616e8457bdc26cc6dceb6 (diff) | |
parent | dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 5 |
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 |