Commit 131e53d4 authored by Robbert Krebbers's avatar Robbert Krebbers

Give WExpr instance for Rec lower priority so it does not go

through definitions.
parent 35f151a0
Pipeline #925 passed with stage
......@@ -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
......
......@@ -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 *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment