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

Name a variable in a `destruct`.

parent b433bf12
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/coq_tactics.v
+ 1
− 1
View file @ d2a0e5d1
...@@ -841,7 +841,7 @@ Lemma tac_löb Δ i Q : ...@@ -841,7 +841,7 @@ Lemma tac_löb Δ i Q :
end → end →
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
destruct (envs_app _ _ _) eqn:?; last done. destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
rewrite envs_entails_eq => ?? HQ. rewrite envs_entails_eq => ?? HQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //. rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine. rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
......
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