Skip to content
Snippets Groups Projects
Commit 66cb81f2 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Renaming monPred_ofe -> monPredC.

parent 3570accc
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 3 deletions
theories/bi/monpred.v
+ 3
− 3
View file @ 66cb81f2
...@@ -52,9 +52,9 @@ Section Ofe_Cofe_def. ...@@ -52,9 +52,9 @@ Section Ofe_Cofe_def.
Definition monPred_ofe_mixin : OfeMixin monPred. Definition monPred_ofe_mixin : OfeMixin monPred.
Proof. by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist). Qed. Proof. by apply (iso_ofe_mixin monPred_sig monPred_sig_equiv monPred_sig_dist). Qed.
Canonical Structure monPred_ofe := OfeT monPred monPred_ofe_mixin. Canonical Structure monPredC := OfeT monPred monPred_ofe_mixin.
Global Instance monPred_cofe `{Cofe PROP} : Cofe monPred_ofe. Global Instance monPred_cofe `{Cofe PROP} : Cofe monPredC.
Proof. Proof.
unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_car _ _ _); unshelve refine (iso_cofe_subtype (A:=I-c>PROP) _ MonPred monPred_car _ _ _);
[apply _|by apply monPred_sig_dist|done|]. [apply _|by apply monPred_sig_dist|done|].
...@@ -98,7 +98,7 @@ End Ofe_Cofe. ...@@ -98,7 +98,7 @@ End Ofe_Cofe.
Arguments monPred _ _ : clear implicits. Arguments monPred _ _ : clear implicits.
Local Existing Instance monPred_mono. Local Existing Instance monPred_mono.
Arguments monPred_ofe _ _ : clear implicits. Arguments monPredC _ _ : clear implicits.
(** BI and SBI structures. *) (** BI and SBI structures. *)
......
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