diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 15:09:57 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 15:09:57 +0000 |
commit | 69b3a4294ff715516b808c2eea54c2ccad0f1c12 (patch) | |
tree | 6991a628b2a285623b7e023b8643e62b947025ee | |
parent | 94b339bf87be43fc3b8ef4ef84aa1281e8480d02 (diff) |
adaptation a la nouvelle syntaxe Extract Inlined Constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2001 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | contrib/extraction/test/extract_reals | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/contrib/extraction/test/extract_reals b/contrib/extraction/test/extract_reals index 4d15cc4e8..9cb14ef45 100755 --- a/contrib/extraction/test/extract_reals +++ b/contrib/extraction/test/extract_reals @@ -3,16 +3,16 @@ 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". +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` |