aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-07 15:36:09 +0000
committerGravatar fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-07-07 15:36:09 +0000
commitd8d585d692880cfb1a9af7245346dc43d515319d (patch)
tree897531d87362d68f417772ad868676199fa22686 /Makefile.common
parentcf69befd5678b6827126ef0a2b89218ea7b02c89 (diff)
Micromega: doc + test-suite update
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common
index 97f57822f..915f383e0 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -88,7 +88,7 @@ REFMANCOQTEXFILES:=\
doc/refman/RefMan-oth.v.tex doc/refman/RefMan-ltac.v.tex \
doc/refman/RefMan-decl.v.tex \
doc/refman/Cases.v.tex doc/refman/Coercion.v.tex doc/refman/Extraction.v.tex \
- doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Polynom.v.tex \
+ doc/refman/Program.v.tex doc/refman/Omega.v.tex doc/refman/Micromega.v.tex doc/refman/Polynom.v.tex \
doc/refman/Setoid.v.tex doc/refman/Helm.tex doc/refman/Classes.v.tex
REFMANTEXFILES:=\