Commit 629385ee authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

MakeEmbed does not need BiEmbedding. It only needs BiEmbed.

parent aa5b93f6
......@@ -398,14 +398,14 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
would typically try to instantiate this evar with some arbitrary
logical constructs such as emp or True. Therefore, we use an Hint
Mode to disable all the instances that would have this behavior. *)
Class MakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : P Q.
Arguments MakeEmbed {_ _ _ _} _%I _%I.
Hint Mode MakeEmbed + + + + - - : typeclass_instances.
Class KnownMakeEmbed `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
Arguments MakeEmbed {_ _ _} _%I _%I.
Hint Mode MakeEmbed + + + - - : typeclass_instances.
Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
known_make_embed :> MakeEmbed P Q.
Arguments KnownMakeEmbed {_ _ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + + ! - : typeclass_instances.
Arguments KnownMakeEmbed {_ _ _} _%I _%I.
Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P Q PQ .
Arguments MakeSep {_} _%I _%I _%I.
......
......@@ -94,4 +94,11 @@ Section tests.
Proof.
iIntros. iFrame. by iApply fupd_intro_mask'.
Qed.
Lemma test_iFrame_embed_persistent (P : PROP) (Q: monPred) :
Q P Q P P.
Proof.
iIntros "[$ #HP]". iFrame "HP".
Qed.
End tests.
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