From cd51195076511bb3a159896ec9fd501de09d5ebc Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Mon, 11 Oct 2021 09:27:16 +0200 Subject: [PATCH] Fix indentation. --- iris/proofmode/class_instances_later.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v index e1a37c576..b38a3094d 100644 --- a/iris/proofmode/class_instances_later.v +++ b/iris/proofmode/class_instances_later.v @@ -190,7 +190,7 @@ Global Instance from_forall_later {A} P (Φ : A → PROP) name : Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed. Global Instance from_forall_laterN {A} P (Φ : A → PROP) n name : - FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name. + FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name. Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed. Global Instance from_forall_except_0 {A} P (Φ : A → PROP) name : -- GitLab