Skip to content

GitLab

Commit 650261fc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Remove spurious `iStartProof`.

parent b6269993
Show whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
theories/proofmode/tactics.v
View file @ 650261fc
...@@ -1263,7 +1263,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) := ...@@ -1263,7 +1263,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
| 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H | 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
| S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n' | S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
end in end in
intros; iStartProof; go n in intros; go n in
lazymatch type of lem with lazymatch type of lem with
| nat => intro_destruct lem | nat => intro_destruct lem
| Z => (* to make it work in Z_scope. We should just be able to bind | Z => (* to make it work in Z_scope. We should just be able to bind
......
Markdown is supported
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