From f5e33af81f56253ba777cde96831ef23f25addba Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 11 Sep 2018 17:18:45 +0200
Subject: Zify: replace local definitions by equations

---
 test-suite/success/ROmega4.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v
index 58ae5b8fb8..a724592749 100644
--- a/test-suite/success/ROmega4.v
+++ b/test-suite/success/ROmega4.v
@@ -3,12 +3,12 @@
     See also #148 for the corresponding improvement in Omega.
 *)
 
-Require Import ZArith ROmega.
+Require Import ZArith Lia.
 Open Scope Z.
 
 Goal let x := 3 in x = 3.
 intros.
-romega.
+lia.
 Qed.
 
 (** Example seen in #4132
@@ -22,5 +22,5 @@ Lemma foo
   (H : - zxy' <= zxy)
   (H' : zxy' <= x') : - b <= zxy.
 Proof.
-romega.
+lia.
 Qed.
-- 
cgit v1.2.3