Commit 6567b894 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix small naming inconsistency.

parent c5815ae5
......@@ -42,7 +42,7 @@ Section bi_embedding.
Global Instance bi_embed_proper : Proper (() ==> ()) bi_embed.
Proof. apply (ne_proper _). Qed.
Global Instance bi_embed_mono_flip : Proper (flip () ==> flip ()) bi_embed.
Global Instance bi_embed_flip_mono : Proper (flip () ==> flip ()) bi_embed.
Proof. solve_proper. Qed.
Global Instance bi_embed_inj : Inj () () bi_embed.
Proof.
......
......@@ -416,7 +416,7 @@ Implicit Types P Q : monPred.
Global Instance monPred_at_mono :
Proper (() ==> () ==> ()) monPred_at.
Proof. by move=> ?? [?] ?? ->. Qed.
Global Instance monPred_at_mono_flip :
Global Instance monPred_at_flip_mono :
Proper (flip () ==> flip () ==> flip ()) monPred_at.
Proof. solve_proper. Qed.
......@@ -426,7 +426,7 @@ Global Instance monPred_in_proper (R : relation I) :
Proof. unseal. split. solve_proper. Qed.
Global Instance monPred_in_mono : Proper (flip () ==> ()) (@monPred_in I PROP).
Proof. unseal. split. solve_proper. Qed.
Global Instance monPred_in_mono_flip : Proper (() ==> flip ()) (@monPred_in I PROP).
Global Instance monPred_in_flip_mono : Proper (() ==> flip ()) (@monPred_in I PROP).
Proof. solve_proper. Qed.
Global Instance monPred_positive : BiPositive PROP BiPositive monPredI.
......
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