Skip to content
Snippets Groups Projects
Commit bf73b3b9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make iDestruct/iMod/... perform an `iStartProof` to get better error messages.

parent 24ea529a
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
− 0
View file @ bf73b3b9
...@@ -1274,6 +1274,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) := ...@@ -1274,6 +1274,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
Also, rule out cases in which it does not make sense to copy, namely when Also, rule out cases in which it does not make sense to copy, namely when
destructing a lemma (instead of a hypothesis) or a spatial hyopthesis destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
(which cannot be kept). *) (which cannot be kept). *)
iStartProof;
lazymatch ident with lazymatch ident with
| None => iPoseProofCore lem as p false tac | None => iPoseProofCore lem as p false tac
| Some ?H => | Some ?H =>
......
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