Commit 485c6b54 authored by Pierre Roux's avatar Pierre Roux

Interface layer for primitive floats in Coq

parent 3cba812b
......@@ -28,6 +28,8 @@ FILES = \
Prop/Double_rounding.v \
IEEE754/Binary.v \
IEEE754/Bits.v \
PrimitiveFloats/SpecLayer.v \
PrimitiveFloats/NativeLayer.v \
Pff/Pff.v \
Pff/Pff2FlocqAux.v \
Pff/Pff2Flocq.v
......@@ -125,7 +127,7 @@ install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop IEEE754 Pff; do mkdir -p @libdir@/$d; done
for d in Core Calc Prop IEEE754 Pff PrimitiveFloats; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
for f in $(FILES); do cp src/$f @libdir@/$f; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
......
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment