From 88679d3e4aab5a3f385e3be28b591f81639d2ae4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 18 Feb 2016 11:26:17 +0100
Subject: [PATCH] Tweak closed proof in heap_lang/tests.

---
 heap_lang/tests.v | 17 +++++------------
 1 file changed, 5 insertions(+), 12 deletions(-)

diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 76fc530c8..afc88d836 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -80,25 +80,18 @@ Section LiftingTests.
 End LiftingTests.
 
 Section ClosedProofs.
-  
   Definition Σ : iFunctorG := λ _, authF (constF heapRA).
+  Notation iProp := (iPropG heap_lang Σ).
 
-  Local Instance : inG heap_lang Σ (authRA heapRA).
-  Proof. by exists 1%nat. Qed.
-
-  (* TODO: Why do I even have to explicitly do this? *)
-  Local Instance : authG heap_lang Σ heapRA.
-  Proof. split; by apply _. Qed.
-  
-  Local Notation iProp := (iPropG heap_lang Σ).
+  Instance: authG heap_lang Σ heapRA.
+  Proof. split; try apply _. by exists 1%nat. Qed.
 
   Lemma heap_e_hoare σ : {{ ownP σ : iProp }} heap_e @ ⊤ {{ λ v, v = '2 }}.
   Proof.
     apply ht_alt. rewrite (heap_alloc ⊤ nroot); last by rewrite nclose_nroot.
-    apply wp_strip_pvs, exist_elim=>?. rewrite and_elim_l.
+    apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
   Qed.
 
   Print Assumptions heap_e_hoare.
-    
-End ClosedProofs.  
+End ClosedProofs.
-- 
GitLab