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

Merge branch 'master' of https://gitlab.mpi-sws.org/iris/iris

parents c52b1300 72f54819
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 @ 25818962
...@@ -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