blob: 92749ff0a669503b021f6c0a028381d1602dab3e (
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
28
29
30
31
|
#!/bin/sh
rm -f /tmp/extr$$.v
cat > /tmp/extr$$.v << EOF
Cd "theories/Reals".
Require Reals.
Extract Constant R => float.
Extract Constant R0 => "0.0".
Extract Constant R1 => "1.0".
Extract Constant Rplus => "(+.)".
Extract Constant Rmult => "( *.)".
Extract Constant Ropp => "(~-.)".
Extract Constant Rinv => "(fun x -> 1.0 /. x)".
Extract Constant Rlt => "(<)".
Extract Constant up => "AddReals.my_ceil".
Extract Constant total_order_T => "AddReals.total_order_T".
Extraction Module Rdefinitions.
Extraction Module TypeSyntax.
Extraction Module Raxioms.
Extraction Module Rbase.
Extraction Module R_Ifp.
Extraction Module Rbasic_fun.
Extraction Module Rlimit.
Extraction Module Rfunctions.
Extraction Module Rderiv.
EOF
../../../bin/coqtop.opt -silent -batch -load-vernac-source /tmp/extr$$.v
out=$?
rm -f /tmp/extr$$.v
exit $out
|
