From db1118603214d8af47506a7d476d5a111cbad67b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Jun 2021 11:50:22 +0200
Subject: [PATCH] Fix priority of `Permutation_app'`.

This is a workaround for https://github.com/coq/coq/issues/14571

This fixes #114.
---
 theories/list.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 0e220fd3..80e43e1a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4,6 +4,13 @@ From Coq Require Export Permutation.
 From stdpp Require Export numbers base option.
 From stdpp Require Import options.
 
+(** FIXME: Workaround for https://github.com/coq/coq/issues/14571 *)
+(** Remove the instance [Permutation_app'], since its priority is 10, which is
+above the priority 5 of [proper_relation], and add it back with the right
+priority (default = 0, since the instance has no premises). *)
+Global Remove Hints Permutation_app' : typeclass_instances.
+Global Existing Instance Permutation_app'.
+
 (* Pick up extra assumptions from section parameters. *)
 Set Default Proof Using "Type*".
 
-- 
GitLab