From 243a22e9fa5464641c2b83c020ea6b34611cf061 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Mar 2023 09:51:21 +0100
Subject: [PATCH] Some more indentation.

---
 iris/si_logic/bi.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/iris/si_logic/bi.v b/iris/si_logic/bi.v
index 40464d70f..e0ac0abbf 100644
--- a/iris/si_logic/bi.v
+++ b/iris/si_logic/bi.v
@@ -177,13 +177,13 @@ Proof. done. Qed.
 
 Module siProp.
 Section restate.
-Lemma pure_soundness φ : (⊢@{siPropI} ⌜ φ ⌝) → φ.
-Proof. apply pure_soundness. Qed.
+  Lemma pure_soundness φ : (⊢@{siPropI} ⌜ φ ⌝) → φ.
+  Proof. apply pure_soundness. Qed.
 
-Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{siPropI} x ≡ y) → x ≡ y.
-Proof. apply internal_eq_soundness. Qed.
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{siPropI} x ≡ y) → x ≡ y.
+  Proof. apply internal_eq_soundness. Qed.
 
-Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
-Proof. apply later_soundness. Qed.
+  Lemma later_soundness (P : siProp) : (⊢ ▷ P) → ⊢ P.
+  Proof. apply later_soundness. Qed.
 End restate.
 End siProp.
-- 
GitLab