From d1e00bb24abb5045aad35723722c2b0ae7a0a8aa Mon Sep 17 00:00:00 2001
From: Lysxia
Date: Sun, 22 Mar 2020 17:42:28 -0400
Subject: Sorting: Swap the names of Sorted_sort and LocallySorted_sort

---
 theories/Sorting/Mergesort.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Sorting')

diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v
index a761dba62d..f629c7426b 100644
--- a/theories/Sorting/Mergesort.v
+++ b/theories/Sorting/Mergesort.v
@@ -230,13 +230,13 @@ Proof.
     apply IHl.
 Qed.
 
-Theorem Sorted_sort : forall l, Sorted (sort l).
+Theorem LocallySorted_sort : forall l, Sorted (sort l).
 Proof.
 intro; apply Sorted_iter_merge. constructor.
 Qed.
 
-Corollary LocallySorted_sort : forall l, Sorted.Sorted leb (sort l).
-Proof. intro; eapply Sorted_LocallySorted_iff, Sorted_sort; auto. Qed.
+Corollary Sorted_sort : forall l, Sorted.Sorted leb (sort l).
+Proof. intro; eapply Sorted_LocallySorted_iff, LocallySorted_sort; auto. Qed.
 
 Theorem Permuted_sort : forall l, Permutation l (sort l).
 Proof.
@@ -245,7 +245,7 @@ Qed.
 
 Corollary StronglySorted_sort : forall l,
   Transitive leb -> StronglySorted leb (sort l).
-Proof. auto using Sorted_StronglySorted, LocallySorted_sort. Qed.
+Proof. auto using Sorted_StronglySorted, Sorted_sort. Qed.
 
 End Sort.
 
-- 
cgit v1.2.3