aboutsummaryrefslogtreecommitdiff
path: root/src/Util/NatUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/NatUtil.v')
-rw-r--r--src/Util/NatUtil.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 80169c784..087f0a6c7 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,6 +1,6 @@
Require Coq.Logic.Eqdep_dec.
Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
-Require Import Coq.micromega.Psatz.
+Require Import Coq.micromega.Lia.
Import Nat.
Scheme Equality for nat.