blob: 9cb14ef458e621be223d665c786793ac7a4a26d3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
#!/bin/sh
rm -f /tmp/extr$$.v
cat > /tmp/extr$$.v << EOF
Cd "theories/Reals".
Require Reals.
Extract Inlined Constant R => float.
Extract Inlined Constant R0 => "0.0".
Extract Inlined Constant R1 => "1.0".
Extract Inlined Constant Rplus => "(+.)".
Extract Inlined Constant Rmult => "( *.)".
Extract Inlined Constant Ropp => "(~-.)".
Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)".
Extract Inlined Constant Rlt => "(<)".
Extract Inlined Constant up => "AddReals.my_ceil".
Extract Inlined Constant total_order_T => "AddReals.total_order_T".
EOF
for f in $*; do
ff=`basename $f .vo`
echo "Require $ff." >> /tmp/extr$$.v
echo "Extraction Module $ff." >> /tmp/extr$$.v
done
../../../bin/coqtop.opt -silent -batch -load-vernac-source /tmp/extr$$.v
out=$?
#rm -f /tmp/extr$$.v
exit $out
|
