Commit 0135f46c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Eval hnf in iProof like in iPoseProof.

parent 5bd2042e
...@@ -45,9 +45,13 @@ Ltac iMatchGoal tac := ...@@ -45,9 +45,13 @@ Ltac iMatchGoal tac :=
Tactic Notation "iProof" := Tactic Notation "iProof" :=
lazymatch goal with lazymatch goal with
| |- of_envs _ _ => fail "iProof: already in Iris proofmode" | |- of_envs _ _ => fail "iProof: already in Iris proofmode"
| |- True _ => apply tac_adequate | |- ?P =>
| |- _ _ => apply uPred.wand_entails, tac_adequate match eval hnf in P with
| |- _ _ => apply uPred.iff_equiv, tac_adequate | True _ => apply tac_adequate
| _ _ => apply uPred.wand_entails, tac_adequate
(* need to use the unfolded version of [⊣⊢] due to the hnf *)
| uPred_equiv' _ _ => apply uPred.iff_equiv, tac_adequate
end
end. end.
(** * Context manipulation *) (** * Context manipulation *)
......
Supports Markdown
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