diff --git a/msl/subtypes.v b/msl/subtypes.v
index dbbac1586..114c7f340 100644
--- a/msl/subtypes.v
+++ b/msl/subtypes.v
@@ -3,12 +3,11 @@
  *
  *)
 
+Require Import Arith.
 Require Import VST.msl.base.
 Require Import VST.msl.ageable.
 Require Import VST.msl.predicates_hered.
 
-Import Arith.
-
 Local Open Scope pred.
 
 Section Fash.
diff --git a/zlist/list_solver.v b/zlist/list_solver.v
index ee8289057..612d8a5dd 100644
--- a/zlist/list_solver.v
+++ b/zlist/list_solver.v
@@ -1,3 +1,4 @@
+Require Import RelationClasses.
 Require Import ZArith Znumtheory.
 Require Import Coq.Lists.List.
 Require Import Lia.
@@ -1030,8 +1031,8 @@ Section Sorted.
 Variable A : Type.
 Variable d : Inhabitant A.
 Variable le : A -> A -> Prop.
-Context {Hrefl : Relations_1.Reflexive A le}.
-Context {Htrans : Relations_1.Transitive le}.
+Context {Hrefl : Reflexive le}.
+Context {Htrans : Transitive le}.
 
 Definition sorted (l : list A) :=
   forall i j, 0 <= i <= j /\ j < Zlength l -> le (Znth i l) (Znth j l).