From 4882ecf8a3fb0c689309f0e37ff87dd25e5a0a7e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 14:36:44 +0100
Subject: [PATCH] Shorten some stuff in heap_lang.

---
 barrier/heap_lang.v | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index aca91e51b..25bc98d83 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.
-- 
GitLab