From 6c5551d0782d78ab7ed182480ba18836a3f6dae7 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 30 Mar 2020 12:20:49 +0200
Subject: ZArith: move lia hints to a dedicated module

---
 test-suite/bugs/closed/bug_1912.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v
index 987a541778..0228abbb9b 100644
--- a/test-suite/bugs/closed/bug_1912.v
+++ b/test-suite/bugs/closed/bug_1912.v
@@ -1,4 +1,4 @@
-Require Import ZArith.
+Require Import Omega.
 
 Goal forall x, Z.succ (Z.pred x) = x.
 intros x.
-- 
cgit v1.2.3