From 8af241185ffc63efb00e0c10efec2b5df9a7594e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 May 2019 09:29:38 +0200
Subject: [PATCH] Fix.

---
 tests/atomic.8.8.ref   | 6 ++++++
 tests/list_reverse.ref | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
index a3f918527..ced301792 100644
--- a/tests/atomic.8.8.ref
+++ b/tests/atomic.8.8.ref
@@ -6,6 +6,7 @@
   Q : iProp Σ
   l : loc
   v : val
+  IPM_INTERNAL : IPM_STATE 3
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
@@ -36,6 +37,7 @@
   heapG0 : heapG Σ
   P : val → iProp Σ
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << ∀ x : val, P x
               ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
@@ -68,6 +70,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << ∀ x : val, l ↦ x
               ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
@@ -99,6 +102,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅
@@ -131,6 +135,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
@@ -196,6 +201,7 @@
   heapG0 : heapG Σ
   l : loc
   Φ : language.val heap_lang → iProp Σ
+  IPM_INTERNAL : IPM_STATE 1
   ============================
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
          << ∃ yyyy : val, l ↦ yyyy
diff --git a/tests/list_reverse.ref b/tests/list_reverse.ref
index 2c8d90077..430c8ed8f 100644
--- a/tests/list_reverse.ref
+++ b/tests/list_reverse.ref
@@ -5,6 +5,7 @@
   hd, acc : val
   xs, ys : list val
   Φ : val → iPropI Σ
+  IPM_INTERNAL : IPM_STATE 2
   ============================
   "Hxs" : is_list hd xs
   "Hys" : is_list acc ys
@@ -16,6 +17,7 @@
   
   Σ : gFunctors
   heapG0 : heapG Σ
+  IPM_INTERNAL : IPM_STATE 2
   acc : val
   ys : list val
   Φ : val → iPropI Σ
-- 
GitLab