Skip to content
Snippets Groups Projects
Commit 2fabfd72 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Ralf Jung
Browse files

Remove %I which is implied

parent 6f18e8cd
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
iris/base_logic/upred.v
+ 1
− 1
View file @ 2fabfd72
...@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred { ...@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred {
this way. *) this way. *)
Local Coercion uPred_holds : uPred >-> Funclass. Local Coercion uPred_holds : uPred >-> Funclass.
Bind Scope bi_scope with uPred. Bind Scope bi_scope with uPred.
Global Arguments uPred_holds {_} _%I _ _ : simpl never. Global Arguments uPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred. Add Printing Constructor uPred.
Global Instance: Params (@uPred_holds) 3 := {}. Global Instance: Params (@uPred_holds) 3 := {}.
......
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