Commit cb429ab7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Also fix `Permutation_cons`.

parent db111860
Pipeline #49502 passed with stage
in 4 minutes and 58 seconds
......@@ -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*".
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment