Commit f448aed5 authored by Michael Sammler's avatar Michael Sammler
Browse files

Revert "remove li_let_bind for wand"

This reverts commit 6e03a868.
parent 6e03a868
......@@ -99,8 +99,8 @@ Ltac liRIntroduceLetInGoal :=
lazymatch goal with
| |- @envs_entails ?PROP ?Δ ?P =>
lazymatch P with
(* | @bi_wand ?PROP ?Q ?T => *)
(* li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@bi_wand PROP Q H))) *)
| @bi_wand ?PROP ?Q ?T =>
li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@bi_wand PROP Q H)))
| @typed_val_expr ?Σ ?tG ?e ?T =>
li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_val_expr Σ tG e H)))
| @typed_write ?Σ ?tG ?b ?e ?ot ?v ?ty ?Mov ?T =>
......
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