From 5797fbef14b1593c85f221bb8712ecb7a536216b Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sat, 31 May 2025 00:55:07 -0400 Subject: [PATCH] use RelationClasses instead of Relations_1 in Sorting --- theories/Sorting/Sorted.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 9f4c17108c..dd9182f6f7 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -20,7 +20,7 @@ The two notions are equivalent if the order is transitive. *) -From Stdlib Require Import List Relations Relations_1. +From Stdlib Require Import List Relations RelationClasses. (* Set Universe Polymorphism. *) @@ -29,7 +29,7 @@ From Stdlib Require Import List Relations Relations_1. Set Implicit Arguments. Local Notation "[ ]" := nil (at level 0). Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0). -Arguments Transitive [U] R. +Local Arguments Transitive [_] R. Section defs.