From 6e22d9105111b91e275fb7ca1142f0185048939f Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 14 Jul 2022 15:16:10 -0400 Subject: [PATCH] explain why IntoLaterN uses MakeLaterN --- iris/proofmode/class_instances_later.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v index 09d0cf4d0..c27ebf69d 100644 --- a/iris/proofmode/class_instances_later.v +++ b/iris/proofmode/class_instances_later.v @@ -282,6 +282,10 @@ Global Instance into_laterN_later only_head n n' m' P Q lQ : progress, but there may still be a left-over (i.e. [n']) to cancel more deeply into [P], as such, we continue with [MaybeIntoLaterN]. *) TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) → + (* Similar to [iFrame], the [iNext] tactic also performs a traversal through a + term (a hypothesis) to find laters to strip. And like [iFrame] we don't want + this to be excessively smart. So we use the same typeclass as [iFrame] here. + *) MakeLaterN m' Q lQ → IntoLaterN only_head n (▷ P) lQ | 2. Proof. -- GitLab