From 446b265f5d1f6e6828a7f653b1f648ebdf768321 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Jul 2017 12:21:37 +0200
Subject: Recognizing Z in romega up to conversion.

---
 test-suite/bugs/closed/4717.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'test-suite')

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