Commit f2878896 authored by Ralf Jung's avatar Ralf Jung

Plain typeclass should not require BiPlainly instance to be inferred

parent b65cf679
......@@ -86,7 +86,7 @@ End plainly_laws.
Class Plain `{BiPlainly PROP} (P : PROP) := plain : P P.
Arguments Plain {_ _} _%I : simpl never.
Arguments plain {_ _} _%I {_}.
Hint Mode Plain + ! ! : typeclass_instances.
Hint Mode Plain + - ! : typeclass_instances.
Instance: Params (@Plain) 1.
Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
......
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