Confusing result by `wp_op`
As reported in private by @birkedal:
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Definition test `{heapG Σ} (n : nat) (v : val) :
(WP if: #n = v then #true else #false {{ _, True }})%I.
Proof.
wp_op.This gives
bin_op_eval EqOp #n v = Some ?Goal0
______________________________________(2/2)
--------------------------------------∗
WP if: ?Goal0 then #true else #false {{ _, True }}Pre !97 (merged) this used to work because bin_op_eval used to match first on the operations and then on the operand. Right now, it first matches on the operands, and only then on the operation.