diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v index e013e24069bf117c7d4fa94dd888f48b3f428236..ee84ce46d843193eae6fa032d404a8e68c91b6a2 100644 --- a/iris/proofmode/class_instances_embedding.v +++ b/iris/proofmode/class_instances_embedding.v @@ -215,7 +215,7 @@ Global Instance into_embed_affinely IntoEmbed P Q → IntoEmbed (<affine> P) (<affine> Q). Proof. rewrite /IntoEmbed=> ->. by rewrite embed_affinely_2. Qed. -Global Instance into_later_embed`{!BiEmbedLater PROP PROP'} n P Q : +Global Instance into_later_embed `{!BiEmbedLater PROP PROP'} n P Q : IntoLaterN false n P Q → IntoLaterN false n ⎡P⎤ ⎡Q⎤. Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite embed_laterN. Qed. End class_instances_embedding.