Commit 75c98fae authored by Ralf Jung's avatar Ralf Jung

Merge branch 'gen_proofmode' of https://gitlab.mpi-sws.org/FP/iris-coq into gen_proofmode

parents 020ad55d 753de83e
......@@ -969,8 +969,8 @@ Tactic Notation "iModCore" constr(H) :=
eapply tac_modal_elim with _ H _ _ _ _ _;
[env_reflexivity || fail "iMod:" H "not found"
|apply _ ||
let P := match goal with |- ElimModal ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ ?Q _ => Q end in
let P := match goal with |- ElimModal _ ?P _ _ _ => P end in
let Q := match goal with |- ElimModal _ _ _ ?Q _ => Q end in
fail "iMod: cannot eliminate modality " P "in" Q
|try fast_done (* optional side-condition *)
|env_reflexivity|].
......
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