From 6ec855ab6053d289609086dc43d1bb208f0789b4 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg <jihgfee@gmail.com>
Date: Wed, 15 Apr 2020 12:39:05 +0200
Subject: [PATCH] Fixed a spacing issue in metatheory.v

---
 theories/heap_lang/metatheory.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/heap_lang/metatheory.v b/theories/heap_lang/metatheory.v
index ea41ee2d4..0402c7eb7 100644
--- a/theories/heap_lang/metatheory.v
+++ b/theories/heap_lang/metatheory.v
@@ -84,7 +84,7 @@ Lemma subst_rec_ne' f y e x v :
   subst' x v (Rec f y e) = Rec f y (subst' x v e).
 Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
 
-Lemma  bin_op_eval_closed op v1 v2 v':
+Lemma bin_op_eval_closed op v1 v2 v' :
   is_closed_val v1 → is_closed_val v2 → bin_op_eval op v1 v2 = Some v' →
   is_closed_val v'.
 Proof.
@@ -124,7 +124,6 @@ Lemma head_step_is_closed e1 σ1 obs e2 σ2 es :
   is_closed_expr [] e1 →
   map_Forall (λ _ v, is_closed_val v) σ1.(heap) →
   head_step e1 σ1 obs e2 σ2 es →
-
   is_closed_expr [] e2 ∧ Forall (is_closed_expr []) es ∧
   map_Forall (λ _ v, is_closed_val v) σ2.(heap).
 Proof.
-- 
GitLab