From 742e3e1ad1414ec74efa6fbcffeb37b82562daac Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 20 Oct 2020 16:37:51 +0200 Subject: [PATCH] Fix `Params` instance for views. Thanks @Blaisorblade for reporting. --- theories/algebra/view.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/algebra/view.v b/theories/algebra/view.v index 21541b73b..85e9670a9 100644 --- a/theories/algebra/view.v +++ b/theories/algebra/view.v @@ -55,7 +55,7 @@ Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel { }. Arguments ViewRel {_ _} _ _. Arguments view_rel_holds {_ _} _ _ _ _. -Instance: Params (@view_rel) 4 := {}. +Instance: Params (@view_rel_holds) 4 := {}. Instance view_rel_ne {A B} (rel : view_rel A B) n : Proper (dist n ==> dist n ==> iff) (rel n). -- GitLab