From cb429ab77158e260d3586a468bed0ef3998338ed Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 29 Jun 2021 12:26:41 +0200 Subject: [PATCH] Also fix `Permutation_cons`. --- theories/list.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/theories/list.v b/theories/list.v index 80e43e1a..98c9d5ee 100644 --- a/theories/list.v +++ b/theories/list.v @@ -5,11 +5,12 @@ 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'. +(** Remove the instances [Permutation_cons] and [Permutation_app'] since their +priorities are 10, which is above the priority 5 of [proper_relation], and add +them back with the right priority (default = 0, since these instances have no +premises). *) +Global Remove Hints Permutation_cons Permutation_app' : typeclass_instances. +Global Existing Instances Permutation_cons Permutation_app'. (* Pick up extra assumptions from section parameters. *) Set Default Proof Using "Type*". -- GitLab