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

Error message for iAccu.

parent ec42e1d0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/tactics.v
+ 1
− 1
View file @ 7999c5b1
......@@ -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.
Tactic Notation "iAccu" :=
eapply tac_accu; env_reflexivity.
eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar."].
Hint Extern 0 (_ ⊢ _) => iStartProof.
......
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