Commit a4707ed5 authored by Jonas Kastberg's avatar Jonas Kastberg

intropattern -> simple_intropattern

Note: Compatibility with 8.10 not verified yet.
parent f55d64b5
......@@ -229,35 +229,35 @@ Tactic Notation "wp_recv_core" tactic3(tac_intros) "as" tactic3(tac) :=
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" "(" simple_intropattern_list(xs) ")" "as" constr(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" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
wp_recv_core (intros xs) as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
Tactic Notation "wp_recv" "(" intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
Tactic Notation "wp_recv" "(" simple_intropattern_list(xs) ")" "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
......@@ -397,11 +397,11 @@ Tactic Notation "wp_branch_core" "as" tactic3(tac1) tactic3(tac2) :=
Tactic Notation "wp_branch" "as" constr(pat1) "|" constr(pat2) :=
wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iDestructHyp H as pat2).
Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" constr(pat2) :=
Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" constr(pat2) :=
wp_branch_core as (fun H => iPure H as pat1) (fun H => iDestructHyp H as pat2).
Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" intropattern(pat2) :=
Tactic Notation "wp_branch" "as" constr(pat1) "|" "%" simple_intropattern(pat2) :=
wp_branch_core as (fun H => iDestructHyp H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" "as" "%" intropattern(pat1) "|" "%" intropattern(pat2) :=
Tactic Notation "wp_branch" "as" "%" simple_intropattern(pat1) "|" "%" simple_intropattern(pat2) :=
wp_branch_core as (fun H => iPure H as pat1) (fun H => iPure H as pat2).
Tactic Notation "wp_branch" := wp_branch as %_ | %_.
......
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