diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index aca91e51b9fcbe2cfc5b9526a01a007ff0abbe6c..25bc98d831e127c2cad60d3759c7bb57150f0fec 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -287,9 +287,7 @@ Qed.
 Lemma alloc_fresh e v σ :
   let l := fresh (dom _ σ) in
   to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
-Proof.
-  by intros; apply AllocS, (not_elem_of_dom (D:=gset positive)), is_fresh.
-Qed.
+Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
 End heap_lang.
 
@@ -302,8 +300,7 @@ Program Canonical Structure heap_lang : language := {|
 Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
   heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
 
-Global Instance heap_lang_ctx K :
-  LanguageCtx heap_lang (heap_lang.fill K).
+Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
 Proof.
   split.
   * eauto using heap_lang.fill_not_val.