From 0bbf6d6cb22d573f896c0137b54e7b1934bae7de Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres@andres.systems>
Date: Sat, 31 May 2025 13:44:37 -0400
Subject: [PATCH] use RelationClasses instead of old Relations_1 (for
 rocq-prover/stdlib#152)

---
 msl/subtypes.v      | 3 +--
 zlist/list_solver.v | 5 +++--
 2 files changed, 4 insertions(+), 4 deletions(-)

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).