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

Rename constructor of `uPred` into `UPred`.

parent 414cc39a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/upred.v
+ 1
− 1
View file @ da045e6b
...@@ -47,7 +47,7 @@ Local Hint Extern 10 (_ ≤ _) => lia : core. ...@@ -47,7 +47,7 @@ Local Hint Extern 10 (_ ≤ _) => lia : core.
connective. connective.
*) *)
Record uPred (M : ucmraT) : Type := IProp { Record uPred (M : ucmraT) : Type := UPred {
uPred_holds :> nat → M → Prop; uPred_holds :> nat → M → Prop;
uPred_mono n1 n2 x1 x2 : uPred_mono n1 n2 x1 x2 :
......
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