diff --git a/tests/atomic.ref b/tests/atomic.ref index ba5c5ad608616ab2992086c7e9411483ad6fe03e..e1099c9c8af10cf4c4f3bf7dd5b645466e2d6556 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 125a261c18bfaa41ae9246fa617025aa02104174..62e5e23342f7ba3a2721c7a0d3d600859c47d5d7 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.