Commit 582c126c authored by Michael Sammler's avatar Michael Sammler
Browse files

Add li_let_bind for bi_wand (bi_sep _ _)

parent 399716c6
Pipeline #57799 passed with stage
in 11 minutes and 26 seconds
......@@ -790,9 +790,11 @@ Ltac liWand :=
simple notypeclasses refine (tac_do_intro H n' P _ _ _ _ _ _ _); [reduction.pm_reflexivity..|]
] in
lazymatch goal with
| |- envs_entails _ (bi_wand ?P _) =>
| |- envs_entails ?Δ (bi_wand ?P ?T) =>
lazymatch P with
| bi_sep _ _ => notypeclasses refine (tac_wand_sep_assoc _ _ _ _ _)
| bi_sep _ _ =>
li_let_bind T (fun H => constr:(envs_entails Δ (bi_wand P H)));
notypeclasses refine (tac_wand_sep_assoc _ _ _ _ _)
| bi_exist _ => fail "handled by do_forall"
| bi_emp => notypeclasses refine (tac_wand_emp _ _ _)
| bi_pure _ => notypeclasses refine (tac_do_intro_pure _ _ _ _)
......
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