From 7d1f381e7ee2c7183954bed59b44cb70143af4ca Mon Sep 17 00:00:00 2001
From: marijnvanwezel <marijnvanwezel@gmail.com>
Date: Tue, 25 Feb 2025 18:20:44 +0100
Subject: [PATCH] Tweak imports

---
 CHANGELOG.md    | 2 +-
 stdpp/sorting.v | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a685028c..516c417e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -14,7 +14,6 @@ API-breaking change is listed.
 - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
 - Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
-  `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
 - Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
   `StronglySorted_app_2`. Rename lemmas
   `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
@@ -28,6 +27,7 @@ Note that the script is not idempotent, do not run it twice.
 sed -i -E -f- $(find theories -name "*.v") <<EOF
 # length
 s/\bmap_filter_empty_iff\b/map_empty_filter/g
+# StronglySorted
 s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
 s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
 EOF
diff --git a/stdpp/sorting.v b/stdpp/sorting.v
index 57f050a7..f1f787f2 100644
--- a/stdpp/sorting.v
+++ b/stdpp/sorting.v
@@ -1,7 +1,8 @@
 (** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
 standard library, but without using the module system. *)
 From Coq Require Export Sorted.
-From stdpp Require Export orders list sets.
+From stdpp Require Export orders list.
+From stdpp Require Import sets.
 From stdpp Require Import options.
 
 Section merge_sort.
-- 
GitLab