From 4dbfd13eb9b233ce51c98c387ebab73ab172d28e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 22 Aug 2019 21:05:22 +0200
Subject: [PATCH] Apply suggestion to theories/program_logic/ectx_language.v

---
 theories/program_logic/ectx_language.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 73dd0702f..6596fff97 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -179,7 +179,7 @@ Section ectx_language.
   Proof.
     rewrite -not_reducible -not_head_reducible. eauto using head_prim_reducible.
   Qed.
-  Lemma head_prim_fill_reducible_no_obs e  K σ :
+  Lemma head_prim_fill_reducible_no_obs e K σ :
     head_reducible_no_obs e σ → reducible_no_obs (fill K e) σ.
   Proof. intro. by apply fill_reducible_no_obs, head_prim_reducible_no_obs. Qed.
 
-- 
GitLab