Skip to content

Commit 5797fbe

Browse files
committed
use RelationClasses instead of Relations_1 in Sorting
1 parent 94590a1 commit 5797fbe

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

theories/Sorting/Sorted.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@
2020
The two notions are equivalent if the order is transitive.
2121
*)
2222

23-
From Stdlib Require Import List Relations Relations_1.
23+
From Stdlib Require Import List Relations RelationClasses.
2424

2525
(* Set Universe Polymorphism. *)
2626

@@ -29,7 +29,7 @@ From Stdlib Require Import List Relations Relations_1.
2929
Set Implicit Arguments.
3030
Local Notation "[ ]" := nil (at level 0).
3131
Local Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) (at level 0).
32-
Arguments Transitive [U] R.
32+
Local Arguments Transitive [_] R.
3333

3434
Section defs.
3535

0 commit comments

Comments
 (0)