From 381347b553f6c02c1a30d37194c76b15b329e495 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 17 Jun 2021 16:41:23 +0200 Subject: [PATCH] comments; proof style --- iris/bi/lib/laterable.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v index bfc5093c1..797b54a15 100644 --- a/iris/bi/lib/laterable.v +++ b/iris/bi/lib/laterable.v @@ -10,8 +10,8 @@ Global Arguments laterable {_} _%I {_}. Global Hint Mode Laterable + ! : typeclass_instances. (** Proofmode class for turning [P] into a laterable [Q]. - Well be the identity if [P] already is laterable, and add - [make_laterable] otherwise. *) + Will be the identity if [P] already is laterable, and add + [▷] otherwise. *) Class IntoLaterable {PROP : bi} (P Q : PROP) : Prop := { (** This is non-standard; usually we would just demand [P ⊢ make_laterable Q]. However, we need these stronger properties for @@ -224,9 +224,9 @@ Section instances. modality_mixin make_laterable MIEnvId (MIEnvTransform IntoLaterable). Proof. split; simpl; eauto using make_laterable_intro', make_laterable_mono, - make_laterable_sep, intuitionistic_laterable with typeclass_instances. - - intros P Q ?. rewrite (into_laterable P). - apply make_laterable_intro'. eapply (into_laterable_result_laterable P), _. + make_laterable_sep, intuitionistic_laterable with typeclass_instances; []. + intros P Q ?. rewrite (into_laterable P). + apply make_laterable_intro'. eapply (into_laterable_result_laterable P), _. Qed. Definition modality_make_laterable `{!Timeless (PROP:=PROP) emp} := -- GitLab