Skip to content
Snippets Groups Projects
Commit 742e3e1a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix `Params` instance for views.

Thanks @Blaisorblade for reporting.
parent f4060bb5
No related branches found
No related tags found
No related merge requests found
...@@ -55,7 +55,7 @@ Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel { ...@@ -55,7 +55,7 @@ Structure view_rel (A : ofeT) (B : ucmraT) := ViewRel {
}. }.
Arguments ViewRel {_ _} _ _. Arguments ViewRel {_ _} _ _.
Arguments view_rel_holds {_ _} _ _ _ _. 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 : Instance view_rel_ne {A B} (rel : view_rel A B) n :
Proper (dist n ==> dist n ==> iff) (rel n). Proper (dist n ==> dist n ==> iff) (rel n).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment