From eddd2aa6686789ef4ebfcd0f1713fd4a283b111f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 1 Jun 2008 17:34:19 +0000
Subject: BigQ: starting to create and use an interface QSig

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11028 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index 0053dafdcf..b76e9aaf6b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -713,11 +713,14 @@ INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \
 INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \
  $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO)
 
+RATIONALSPECVIAQVO:=$(addprefix theories/Numbers/Rational/SpecViaQ/, \
+ QSig.vo )
+
 RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \
  QMake_base.vo	QpMake.vo	QvMake.vo	Q0Make.vo 	\
  QifMake.vo 	QbiMake.vo 	BigQ.vo )
 
-RATIONALVO:=$(RATIONALBIGQVO)
+RATIONALVO:=$(RATIONALSPECVIAQVO) $(RATIONALBIGQVO)
 
 NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO) $(CYCLICVO) $(RATIONALVO)
 
-- 
cgit v1.2.3