From a1f10626bed1db14ce116e9201ed05dadfc366b4 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 11 Sep 2018 14:32:22 +0200
Subject: Remove romega

---
 test-suite/bugs/closed/4717.v | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v
index 1507fa4bf0..bd9bac37ef 100644
--- a/test-suite/bugs/closed/4717.v
+++ b/test-suite/bugs/closed/4717.v
@@ -19,8 +19,6 @@ Proof.
   omega.
 Qed.
 
-Require Import ZArith ROmega.
-
 Open Scope Z_scope.
 
 Definition Z' := Z.
@@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m,
 Proof.
   intros.
   omega.
-  Undo.
-  romega.
 Qed.
-- 
cgit v1.2.3