diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index abb497d4f23c2c692150bf8ad2ab32775babbf6f..58438403524d6e966f77db01c7a8b82f32f6b5e5 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -115,7 +115,7 @@ Tactic Notation "wp_load" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
-    | Load (Lit (LitLoc ?l)) =>
+    | Load ?l =>
        wp_bind K; eapply tac_wp_load;
          [iAssumption || fail 2 "wp_load: cannot find heap_ctx"
          |done || eauto with ndisj
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index ea9ce4e43a6f5ee73062abeed6e792b4c4c15dfa..50b67fcc52c9c5440411f6d2de33b48ee2d50418 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -16,7 +16,7 @@ Hint Extern 0 (WExpr _ (Var ?y) _) =>
 
 (* Rec *)
 Instance do_wexpr_rec_true {X Y f y e} {H : X `included` Y} er :
-  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er).
+  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er) | 10.
 Proof. intros; red; f_equal/=. by etrans; [apply wexpr_proof_irrel|]. Qed.
 
 (* Values *)