aboutsummaryrefslogtreecommitdiff
path: root/src/Util/CaseUtil.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/CaseUtil.v')
-rw-r--r--src/Util/CaseUtil.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
index 35f207ffc..af04a1e49 100644
--- a/src/Util/CaseUtil.v
+++ b/src/Util/CaseUtil.v
@@ -1,4 +1,4 @@
-Require Import Arith.
+Require Import Coq.Arith.Arith.
Ltac case_max :=
match goal with [ |- context[max ?x ?y] ] =>