Fix issue #181: let `wp_expr_eval` check that the goal is in fact a WP.

  Also, remove the inconsistency that `wp_expr_eval` succeeds on a goal
  that is not a WP.

theories/heap_lang/proofmode.v

@@ -15,11 +15,16 @@ Lemma tac_twp_expr_eval `{heapG Σ} Δ s E Φ e e' :
 Proof. by intros ->. Qed.
 
 Tactic Notation "wp_expr_eval" tactic(t) :=
-  try (
-    iStartProof;
-    first [eapply tac_wp_expr_eval|eapply tac_twp_expr_eval];
-      [let x := fresh in intros x; t; unfold x; reflexivity
-      |]).
+  iStartProof;
+  lazymatch goal with
+  | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+    eapply tac_wp_expr_eval;
+      [let x := fresh in intros x; t; unfold x; reflexivity|]
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
+    eapply tac_twp_expr_eval;
+      [let x := fresh in intros x; t; unfold x; reflexivity|]
+  | _ => fail "wp_expr_eval: not a 'wp'"
+  end.
 
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
@@ -293,13 +298,13 @@ Tactic Notation "wp_apply" open_constr(lem) :=
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
+        wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        twp_bind_core K; iApplyHyp H; wp_expr_simpl) ||
+        twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end