Commit f8ede2b7 authored by Robbert Krebbers's avatar Robbert Krebbers

Version of `wp_recv` without arguments.

parent 538d0804
...@@ -45,6 +45,9 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) := ...@@ -45,6 +45,9 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
| _ => fail "wp_recv: not a 'wp'" | _ => fail "wp_recv: not a 'wp'"
end. end.
Tactic Notation "wp_recv" "as" constr(pat) :=
wp_recv_core (idtac) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" constr(pat) := Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat). wp_recv_core (intros xs) as (fun H => iDestructHyp H as pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")" Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
......
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