Commit 45a78bd3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Comment.

parent a9d41b63
Pipeline #7078 passed with stage
in 23 minutes and 18 seconds
...@@ -389,10 +389,15 @@ Instance maybe_frame_default {PROP : bi} (R P : PROP) : ...@@ -389,10 +389,15 @@ Instance maybe_frame_default {PROP : bi} (R P : PROP) :
TCOr (Affine R) (Absorbing P) MaybeFrame false R P P false | 100. TCOr (Affine R) (Absorbing P) MaybeFrame false R P P false | 100.
Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed. Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
(* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx] variant, (* For each of the [MakeXxxx] class, there is a [KnownMakeXxxx]
that only succeeds if the parameter(s) is not an evar. In the case variant, that only succeeds if the parameter(s) is not an evar. In
the parameter(s) is an evar, then [MakeXxxx] will not instantiate the case the parameter(s) is an evar, then [MakeXxxx] will not
it arbitrarily. *) instantiate it arbitrarily.
The reason for this is that if given an evar, these typeclasses
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 `{BiEmbedding PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : P Q. make_embed : P Q.
Arguments MakeEmbed {_ _ _ _} _%I _%I. Arguments MakeEmbed {_ _ _ _} _%I _%I.
......
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