From 47f94239af69bb260d46c71493392904f14337da Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 2 Feb 2021 17:30:43 +0100
Subject: [PATCH] fix build on old Coq

---
 tests/heap_lang.ref | 8 ++++----
 tests/heap_lang.v   | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index e27e60ad6..0e1632838 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -71,9 +71,9 @@
 "wp_load_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: wp_load: cannot find 'Load' in (Fork Skip).
+Tactic failure: wp_load: cannot find 'Load' in (Fork #()).
 The command has indeed failed with message:
-Tactic failure: wp_load: cannot find 'Load' in (Fork Skip).
+Tactic failure: wp_load: cannot find 'Load' in (Fork #()).
 "wp_load_no_ptsto"
      : string
 The command has indeed failed with message:
@@ -81,9 +81,9 @@ Tactic failure: wp_load: cannot find l ↦ ?.
 "wp_store_fail"
      : string
 The command has indeed failed with message:
-Tactic failure: wp_store: cannot find 'Store' in (Fork Skip).
+Tactic failure: wp_store: cannot find 'Store' in (Fork #()).
 The command has indeed failed with message:
-Tactic failure: wp_store: cannot find 'Store' in (Fork Skip).
+Tactic failure: wp_store: cannot find 'Store' in (Fork #()).
 "wp_store_no_ptsto"
      : string
 The command has indeed failed with message:
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index aed38ac39..2e6e82782 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -151,10 +151,10 @@ Section tests.
 
   Check "wp_load_fail".
   Lemma wp_load_fail :
-    ⊢ WP Fork Skip {{ _, True }}.
+    ⊢ WP Fork #() {{ _, True }}.
   Proof. Fail wp_load. Abort.
   Lemma twp_load_fail :
-    ⊢ WP Fork Skip [{ _, True }].
+    ⊢ WP Fork #() [{ _, True }].
   Proof. Fail wp_load. Abort.
   Check "wp_load_no_ptsto".
   Lemma wp_load_fail_no_ptsto (l : loc) :
@@ -163,10 +163,10 @@ Section tests.
 
   Check "wp_store_fail".
   Lemma wp_store_fail :
-    ⊢ WP Fork Skip {{ _, True }}.
+    ⊢ WP Fork #() {{ _, True }}.
   Proof. Fail wp_store. Abort.
   Lemma twp_store_fail :
-    ⊢ WP Fork Skip [{ _, True }].
+    ⊢ WP Fork #() [{ _, True }].
   Proof. Fail wp_store. Abort.
   Check "wp_store_no_ptsto".
   Lemma wp_store_fail_no_ptsto (l : loc) :
-- 
GitLab