Commit b62bb39a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix issue #45.

parent 763bfe4f
...@@ -1053,29 +1053,38 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ...@@ -1053,29 +1053,38 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "∗" with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) "∗" with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) := Tactic Notation "iLöb" "as" constr (IH) "forall" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros Hs with (iLöbCore as IH). iRevertIntros Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" constr(Hs) := Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1) Hs with (iLöbCore as IH). iRevertIntros(x1) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")" Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) ")"
constr(Hs) := constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2) Hs with (iLöbCore as IH). iRevertIntros(x1 x2) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ")" constr(Hs) := ident(x3) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3) Hs with (iLöbCore as IH). iRevertIntros(x1 x2 x3) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ")" constr(Hs) := ident(x3) ident(x4) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4) Hs with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ident(x5) ")" constr(Hs) := ident(x3) ident(x4) ident(x5) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5) Hs with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ident(x5) ident(x6) ")" constr(Hs) := ident(x3) ident(x4) ident(x5) ident(x6) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" constr(Hs) := ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7) Hs with (iLöbCore as IH).
Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2) Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) := ident(x3) ident(x4) ident(x5) ident(x6) ident(x7) ident(x8) ")" constr(Hs) :=
let Hs := constr:(Hs +:+ "∗") in
iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iLöbCore as IH). iRevertIntros(x1 x2 x3 x4 x5 x6 x7 x8) Hs with (iLöbCore as IH).
(** * Assert *) (** * Assert *)
......
Supports Markdown
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