aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/LraTest.v (renamed from test-suite/success/Fourier.v)10
-rw-r--r--test-suite/unit-tests/.merlin.in (renamed from test-suite/unit-tests/.merlin)0
2 files changed, 6 insertions, 4 deletions
diff --git a/test-suite/success/Fourier.v b/test-suite/success/LraTest.v
index b63bead47..bf3a87da2 100644
--- a/test-suite/success/Fourier.v
+++ b/test-suite/success/LraTest.v
@@ -1,12 +1,14 @@
-Require Import Rfunctions.
-Require Import Fourier.
+Require Import Reals.
+Require Import Lra.
+
+Open Scope R_scope.
Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
-intros; split_Rabs; fourier.
+intros; split_Rabs; lra.
Qed.
Lemma l2 :
forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1.
intros.
-split_Rabs; fourier.
+split_Rabs; lra.
Qed.
diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin.in
index b2279de74..b2279de74 100644
--- a/test-suite/unit-tests/.merlin
+++ b/test-suite/unit-tests/.merlin.in