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

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`