Fix `wp_pure` to call `simpl_subst..` in last goal

Both `simpl_subst` and `try wp_value_head` are now called only in the
last subgoal after applying `tac_wp_pure`.

theories/heap_lang/proofmode.v

@@ -56,8 +56,7 @@ Definition wp_pure (efoc : expr) : tactic :=
       [m: T.apply_         (* PureExec *)
       |T.try fast_done     (* The pure condition for PureExec *)
       |T.apply_            (* IntoLaters *)
-      |T.idtac] &> (* FIXME: If I put the `simpl_subst ...` in this branch, it does not work *)
-    simpl_subst &> T.try wp_value_head
+      |simpl_subst &> T.try wp_value_head]
   ) || M.failwith "wp_pure: cannot find" (* efoc "in" e "or" efoc "is not a reduct" *).
 Tactic Notation "wp_pure" open_constr(efoc) := mrun (wp_pure efoc).