Werid bug with `env_notations` and stdpp's `destruct_and!` tactic.
The following code snippet doesn't work, and destruct_and!
fails:
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
Section test.
Variable A : Type.
Variable wf : A -> bool.
Lemma test x y :
(wf x && wf y) → (wf y && wf x).
Proof.
intros.
destruct_and!.
Abort.
End test.
- If you remove the
env_notations
import than it works fine. - If you place the
env_notations
import inside the proof script it also works. - If you inline the
destruct_and?
tactic it also works.
(using coq 8.8.1, HEAD iris and coq-stdpp)