Merge branch 'ralf/rewrite' into 'master'

avoid relying on rewrite's implicit revert

See merge request iris/iris!643

iris/proofmode/coq_tactics.v

@@ -539,7 +539,7 @@ Lemma tac_pose_proof_hyp Δ i j Q :
 Proof.
   destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; 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 [? ->] <-.
   rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
   by rewrite wand_elim_r.