From cc31e71292491169ffe92a2064d64bfc13ccbc42 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 21 Jan 2023 16:28:04 -0500
Subject: [PATCH] Fix indentation.

---
 iris/program_logic/ectx_language.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/iris/program_logic/ectx_language.v b/iris/program_logic/ectx_language.v
index 1e051b486..9d45388e6 100644
--- a/iris/program_logic/ectx_language.v
+++ b/iris/program_logic/ectx_language.v
@@ -99,10 +99,10 @@ Section ectx_language.
   Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
   Proof. apply ectx_language_mixin. Qed.
   Lemma step_by_val K' K_redex e1' e1_redex σ1 κ e2 σ2 efs :
-      fill K' e1' = fill K_redex e1_redex →
-      to_val e1' = None →
-      head_step e1_redex σ1 κ e2 σ2 efs →
-      ∃ K'', K_redex = comp_ectx K' K''.
+    fill K' e1' = fill K_redex e1_redex →
+    to_val e1' = None →
+    head_step e1_redex σ1 κ e2 σ2 efs →
+    ∃ K'', K_redex = comp_ectx K' K''.
   Proof. apply ectx_language_mixin. Qed.
   Lemma head_ctx_step_val K e σ1 κ e2 σ2 efs :
     head_step (fill K e) σ1 κ e2 σ2 efs → is_Some (to_val e) ∨ K = empty_ectx.
-- 
GitLab