From 3e0931eade2ebbfca23a3884a42dec1d1093db52 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 31 Oct 2018 11:28:11 +0100
Subject: [PATCH] Add comment; fix test tests/heap_lang.v.
---
tests/heap_lang.ref | 2 +-
tests/heap_lang.v | 2 +-
theories/heap_lang/proofmode.v | 7 +++++--
3 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index c50bdef3f..93e269e73 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -118,4 +118,4 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
-Tactic failure: wp_cas_suc: not a 'wp'.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index bd89e2de2..f00723e45 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -186,7 +186,7 @@ Section error_tests.
Check "not_cas".
Lemma not_cas :
- (WP #() {{ _, True }})%I.
+ (WP #() #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Abort.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index b8dd756be..6baede50e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -85,8 +85,11 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| _ => fail "wp_pure: not a 'wp'"
end.
-(* The `;[]` makes sure that no side-condition magically spawns. *)
-Ltac wp_pures := repeat (wp_pure _; []).
+(* TODO: do this in one go, without [repeat]. *)
+Ltac wp_pures :=
+ iStartProof;
+ repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
+ magically spawns. *)
(* The handling of beta-reductions with wp_rec needs special care in
order to allow it to unlock locked `RecV` values: We first put
--
GitLab