Skip to content
Snippets Groups Projects
Commit a18b8e18 authored by Ralf Jung's avatar Ralf Jung
Browse files

avoid relying on rewrite's implicit revert

parent ffcaed52
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/proofmode/coq_tactics.v
+ 1
− 1
View file @ a18b8e18
...@@ -539,7 +539,7 @@ Lemma tac_pose_proof_hyp Δ i j Q : ...@@ -539,7 +539,7 @@ Lemma tac_pose_proof_hyp Δ i j Q :
Proof. Proof.
destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done. destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done. destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
rewrite envs_entails_eq. rewrite envs_lookup_delete_Some in Hlookup *. rewrite envs_entails_eq. move: Hlookup. rewrite envs_lookup_delete_Some.
intros [? ->] <-. intros [? ->] <-.
rewrite envs_lookup_sound' // envs_app_singleton_sound //=. rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
by rewrite wand_elim_r. by rewrite wand_elim_r.
......
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