From 5470da51bd57ec3ef60c304e73507a3cc697c944 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 2 Feb 2016 14:00:15 +0100
Subject: [PATCH] less unnecessary importing

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

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 2410b2f6e..5858915bf 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -309,7 +309,6 @@ 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.
-Import heap_lang.
 
 Global Instance heap_lang_ctx K :
   LanguageCtx heap_lang (heap_lang.fill K).
@@ -322,6 +321,6 @@ Proof.
     destruct (heap_lang.step_by_val
       K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
     rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.
-    exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
+    exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
     econstructor; eauto.
 Qed.
-- 
GitLab