Skip to content
Snippets Groups Projects
Commit 57c4759b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Port `iAssert` to n-ary version.

parent e2d44d02
No related branches found
No related tags found
No related merge requests found
......@@ -1873,38 +1873,16 @@ Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic3(tac) :=
end.
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as pat).
iAssertCore Q with Hs as pat (fun H => iDestructHyp0_ H pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1 x2) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1 x2 x3) pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
"(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
iAssertCore Q with Hs as pat (fun H => iDestructHyp_ H xs pat).
Tactic Notation "iAssert" open_constr(Q) "as" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as pat).
iAssertCore Q as pat (fun H => iDestructHyp0_ H pat).
Tactic Notation "iAssert" open_constr(Q) "as"
"(" simple_intropattern(x1) ")" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as (x1) pat).
Tactic Notation "iAssert" open_constr(Q) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) ")" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as (x1 x2) pat).
Tactic Notation "iAssert" open_constr(Q) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
")" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as (x1 x2 x3) pat).
Tactic Notation "iAssert" open_constr(Q) "as"
"(" simple_intropattern(x1) simple_intropattern(x2) simple_intropattern(x3)
simple_intropattern(x4) ")" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
"(" ne_simple_intropattern_list(xs) ")" constr(pat) :=
iAssertCore Q as pat (fun H => iDestructHyp_ H xs pat).
Tactic Notation "iAssert" open_constr(Q) "with" constr(Hs)
"as" "%" simple_intropattern(pat) :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment