From 131e53d42877224d58d4b9b0608d6f6dfda7a562 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 10 May 2016 18:34:29 +0200
Subject: [PATCH] Give WExpr instance for Rec lower priority so it does not go
 through definitions.

---
 heap_lang/proofmode.v    | 2 +-
 heap_lang/substitution.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index abb497d4f..584384035 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 ea9ce4e43..50b67fcc5 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 *)
-- 
GitLab