From 69b3a4294ff715516b808c2eea54c2ccad0f1c12 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 19 Sep 2001 15:09:57 +0000 Subject: 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 --- contrib/extraction/test/extract_reals | 20 ++++++++++---------- 1 file 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` -- cgit v1.2.3