diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 73dd0702f2ea8fc80e9be41961b8b2be4028cc67..6596fff97a08174d6688812a5ca98e47a46cc2be 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.