Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

24 files changed, 0 insertions, 61 deletions

diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc
deleted file mode 100644
index e7204838..00000000
--- a/contrib/extraction/test/custom/Adalloc
+++ /dev/null
@@ -1,2 +0,0 @@
-Require Import BinNat.
-Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Euclid b/contrib/extraction/test/custom/Euclid
deleted file mode 100644
index a58e3940..00000000
--- a/contrib/extraction/test/custom/Euclid
+++ /dev/null
@@ -1 +0,0 @@
-Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec.
diff --git a/contrib/extraction/test/custom/List b/contrib/extraction/test/custom/List
deleted file mode 100644
index ffee7dc9..00000000
--- a/contrib/extraction/test/custom/List
+++ /dev/null
@@ -1 +0,0 @@
-Extraction NoInline map.
diff --git a/contrib/extraction/test/custom/ListSet b/contrib/extraction/test/custom/ListSet
deleted file mode 100644
index c9bea52a..00000000
--- a/contrib/extraction/test/custom/ListSet
+++ /dev/null
@@ -1 +0,0 @@
-Extraction NoInline set_add set_mem.
diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort
deleted file mode 100644
index 22ab18e3..00000000
--- a/contrib/extraction/test/custom/Lsort
+++ /dev/null
@@ -1,2 +0,0 @@
-Require Import BinNat. 
-Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map
deleted file mode 100644
index f024dbd7..00000000
--- a/contrib/extraction/test/custom/Map
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Import BinNat.
-Extraction NoInline Ndouble Ndouble_plus_one.
-
diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard
deleted file mode 100644
index 5932cf7b..00000000
--- a/contrib/extraction/test/custom/Mapcard
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Plus.
-Extraction NoInline plus_is_one.
-Require Import BinNat.
-Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter
deleted file mode 100644
index 22ab18e3..00000000
--- a/contrib/extraction/test/custom/Mapiter
+++ /dev/null
@@ -1,2 +0,0 @@
-Require Import BinNat. 
-Extraction NoInline Ndouble Ndouble_plus_one.
diff --git a/contrib/extraction/test/custom/R_Ifp b/contrib/extraction/test/custom/R_Ifp
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/R_Ifp
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/R_sqr b/contrib/extraction/test/custom/R_sqr
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/R_sqr
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Ranalysis b/contrib/extraction/test/custom/Ranalysis
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Ranalysis
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Raxioms b/contrib/extraction/test/custom/Raxioms
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Raxioms
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rbase b/contrib/extraction/test/custom/Rbase
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rbase
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rbasic_fun b/contrib/extraction/test/custom/Rbasic_fun
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rbasic_fun
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rdefinitions b/contrib/extraction/test/custom/Rdefinitions
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rdefinitions
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v
deleted file mode 100644
index 45d0a224..00000000
--- a/contrib/extraction/test/custom/Reals.v
+++ /dev/null
@@ -1,17 +0,0 @@
-Require Import 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".
-Extract Inlined Constant sqrt => "sqrt".
-Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))".
-Extract Inlined Constant PI => "3.141593".
-Extract Inlined Constant cos => cos.
-Extract Inlined Constant sin => sin.
-Extract Inlined Constant derive_pt => "(fun f x -> ((f (x+.1E-5))-.(f x))*.1E5)".
diff --git a/contrib/extraction/test/custom/Rfunctions b/contrib/extraction/test/custom/Rfunctions
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rfunctions
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rgeom b/contrib/extraction/test/custom/Rgeom
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rgeom
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rlimit b/contrib/extraction/test/custom/Rlimit
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rlimit
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rseries b/contrib/extraction/test/custom/Rseries
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rseries
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rsigma b/contrib/extraction/test/custom/Rsigma
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rsigma
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/Rtrigo b/contrib/extraction/test/custom/Rtrigo
deleted file mode 100644
index d8f1b3e7..00000000
--- a/contrib/extraction/test/custom/Rtrigo
+++ /dev/null
@@ -1,2 +0,0 @@
-Load "custom/Reals".
-
diff --git a/contrib/extraction/test/custom/ZArith_dec b/contrib/extraction/test/custom/ZArith_dec
deleted file mode 100644
index 2201419e..00000000
--- a/contrib/extraction/test/custom/ZArith_dec
+++ /dev/null
@@ -1 +0,0 @@
-Extraction Inline Dcompare_inf Zcompare_rec.
diff --git a/contrib/extraction/test/custom/fast_integer b/contrib/extraction/test/custom/fast_integer
deleted file mode 100644
index e2b24953..00000000
--- a/contrib/extraction/test/custom/fast_integer
+++ /dev/null
@@ -1 +0,0 @@
-Extraction NoInline Zero_suivi_de Un_suivi_de.