Commit b8938010 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix some bad names.

parent 9d68507d
......@@ -920,10 +920,10 @@ Proof.
- intros P. split=> i /=.
rewrite bi.later_forall. f_equiv=> j. by rewrite -later_plainly_2.
Qed.
Global Instance monPred_plainlyC `{BiPlainly PROP} : BiPlainly monPredSI :=
Global Instance monPred_bi_plainly `{BiPlainly PROP} : BiPlainly monPredSI :=
{| bi_plainly_mixin := monPred_plainly_mixin |}.
Global Instance monPred_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
Global Instance monPred_bi_plainly_exist `{BiPlainly PROP} `{@BiIndexBottom I bot} :
BiPlainlyExist PROP BiPlainlyExist monPredSI.
Proof.
split=>?/=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
......
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