Commit e4110b8e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Typo.

parent 352292a8
Pipeline #7217 passed with stage
in 28 minutes and 21 seconds
......@@ -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" :=
iStartProof; 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.
......
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