From 5312915c1b29929f82e1f8de80609a277584913f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 28 Jun 2012 07:59:03 +0000
Subject: Use Flocq for floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 coq | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'coq')

diff --git a/coq b/coq
index 53ed140..ce3e1ed 100755
--- a/coq
+++ b/coq
@@ -13,5 +13,5 @@ make -q ${1}o || {
    done)
 }
 
-coqide -I lib -I common -I $ARCH/$VARIANT -I $ARCH -I backend -I cfrontend $1 \
+coqide -I lib -I common -I $ARCH/$VARIANT -I $ARCH -I backend -I cfrontend -I flocq -I flocq/Appli -I flocq/Calc -I flocq/Core -I flocq/Prop $1 \
 && make ${1}o
-- 
cgit v1.2.3