Use Flocq for floats

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 1 insertions, 1 deletions

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