Skip to content
Snippets Groups Projects
Commit dbb44a40 authored by Ralf Jung's avatar Ralf Jung
Browse files

consistent non-parentheses for Implicit Types

parent 2abfa296
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/bi/updates.v
+ 2
− 2
View file @ dbb44a40
......@@ -62,7 +62,7 @@ Hint Mode BUpdFacts ! - : typeclass_instances.
Section bupd_derived.
Context `{BUpdFacts PROP}.
Implicit Types (P Q R: PROP).
Implicit Types P Q R: PROP.
(* FIXME: Removing the `PROP:=` diverges. *)
Global Instance bupd_proper : Proper ((≡) ==> (≡)) (bupd (PROP:=PROP)) := ne_proper _.
......@@ -119,7 +119,7 @@ Hint Mode FUpdFacts ! - - : typeclass_instances.
Section fupd_derived.
Context `{FUpdFacts PROP}.
Implicit Types (P Q R: PROP).
Implicit Types P Q R: PROP.
Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (fupd (PROP:=PROP) E1 E2) := ne_proper _.
......
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