From 123aaf49f1bb4eb11c69cc830d86f56cb0fb78d8 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 23 May 2023 23:02:37 +0200 Subject: [PATCH] Missing space. --- iris/proofmode/class_instances_embedding.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v index e013e2406..ee84ce46d 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. -- GitLab