Commit 3e0931ea authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Add comment; fix test tests/heap_lang.v.

parent 079da034
...@@ -118,4 +118,4 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or ...@@ -118,4 +118,4 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
: string : string
The command has indeed failed with message: The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed. Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: not a 'wp'. Tactic failure: wp_cas_suc: cannot find 'CAS' in (#() #()).
...@@ -186,7 +186,7 @@ Section error_tests. ...@@ -186,7 +186,7 @@ Section error_tests.
Check "not_cas". Check "not_cas".
Lemma not_cas : Lemma not_cas :
(WP #() {{ _, True }})%I. (WP #() #() {{ _, True }})%I.
Proof. Proof.
Fail wp_cas_suc. Fail wp_cas_suc.
Abort. Abort.
......
...@@ -85,8 +85,11 @@ Tactic Notation "wp_pure" open_constr(efoc) := ...@@ -85,8 +85,11 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
| _ => fail "wp_pure: not a 'wp'" | _ => fail "wp_pure: not a 'wp'"
end. end.
(* The `;[]` makes sure that no side-condition magically spawns. *) (* TODO: do this in one go, without [repeat]. *)
Ltac wp_pures := repeat (wp_pure _; []). 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 (* The handling of beta-reductions with wp_rec needs special care in
order to allow it to unlock locked `RecV` values: We first put order to allow it to unlock locked `RecV` values: We first put
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment