From 97b83157c307b0f45fafe461c35f120a0bf3346a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Jan 2020 10:55:34 +0100
Subject: [PATCH] adjust atomic test for more Coq compatibility
---
tests/atomic.ref | 4 ++++
tests/atomic.v | 1 +
2 files changed, 5 insertions(+)
diff --git a/tests/atomic.ref b/tests/atomic.ref
index ba5c5ad60..e1099c9c8 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -15,8 +15,12 @@
"non_laterable"
: string
The command has indeed failed with message:
+Ltac call to "iAuIntro" failed.
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
The command has indeed failed with message:
+In nested Ltac calls to "awp_apply (open_constr)",
+"<ssreflect_plugin::ssrtclseq@0> wp_apply_core lem fun H => iApplyHyp H ; last iAuIntro" and
+"iAuIntro", last call failed.
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"printing"
: string
diff --git a/tests/atomic.v b/tests/atomic.v
index 125a261c1..62e5e2334 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -2,6 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
+Set Ltac Backtrace.
Set Default Proof Using "Type".
Section tests.
--
GitLab