work around coq/coq#15596

mit-plv · Feb 7, 2022 · b954274 · b954274
1 parent 68ce343
commit b954274
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 3 deletions.
diff --git a/src/coqutil/Datatypes/List.v b/src/coqutil/Datatypes/List.v
@@ -5,7 +5,7 @@ Require Import coqutil.Z.Lia.
 Require Import coqutil.Datatypes.Option.
 Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Lists.List. Import ListNotations.
-Require Import Coq.Sorting.Permutation.
+Require Import coqutil.Sorting.Permutation.
 
 Definition enumerate [A] start xs := combine (seq start (@length A xs)) xs.
 Definition zip [A B C] (f : A -> B -> C) xs ys :=

diff --git a/src/coqutil/Map/Properties.v b/src/coqutil/Map/Properties.v
@@ -2,7 +2,7 @@ Require Import coqutil.Tactics.autoforward coqutil.Tactics.destr coqutil.Decidab
 Require Import coqutil.Z.Lia.
 Import map.
 Require Import coqutil.Datatypes.Option.
-Require Import Coq.Sorting.Permutation.
+Require Import coqutil.Sorting.Permutation.
 
 Module map.
   Section WithMap. Local Set Default Proof Using "All".

diff --git a/src/coqutil/Sorting/OrderToPermutation.v b/src/coqutil/Sorting/OrderToPermutation.v
@@ -4,7 +4,7 @@
    of the original list. *)
 
 Require Import Coq.Arith.PeanoNat.
-Require Import Coq.Sorting.Permutation Coq.Sorting.Sorting.
+Require Import coqutil.Sorting.Permutation Coq.Sorting.Sorting.
 Require Import coqutil.Tactics.destr.
 Require Import coqutil.Datatypes.List.
 

diff --git a/src/coqutil/Sorting/Permutation.v b/src/coqutil/Sorting/Permutation.v
@@ -0,0 +1,4 @@
+Require Export Coq.Sorting.Permutation.
+(* Workaround for https://github.com/coq/coq/issues/15596 *)
+Global Remove Hints Permutation.Permutation_cons Permutation.Permutation_app' :
+  typeclass_instances.