Skip to content
Snippets Groups Projects
Commit 5392b62f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Add iStartProof in iAccu.

parent 354f2692
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/tactics.v
+ 1
− 1
View file @ 5392b62f
...@@ -1937,7 +1937,7 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern( ...@@ -1937,7 +1937,7 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose. iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
Tactic Notation "iAccu" := Tactic Notation "iAccu" :=
eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar."]. iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar."].
Hint Extern 0 (_ ⊢ _) => iStartProof. Hint Extern 0 (_ ⊢ _) => iStartProof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment