Commit 399716c6 authored by Michael Sammler's avatar Michael Sammler
Browse files

Revert "Revert "remove li_let_bind for wand""

This reverts commit f448aed5.
parent 6970eb20
Pipeline #57797 passed with stage
in 11 minutes and 28 seconds
...@@ -99,8 +99,8 @@ Ltac liRIntroduceLetInGoal := ...@@ -99,8 +99,8 @@ Ltac liRIntroduceLetInGoal :=
lazymatch goal with lazymatch goal with
| |- @envs_entails ?PROP ?Δ ?P => | |- @envs_entails ?PROP ?Δ ?P =>
lazymatch P with lazymatch P with
| @bi_wand ?PROP ?Q ?T => (* | @bi_wand ?PROP ?Q ?T => *)
li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@bi_wand PROP Q H))) (* li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@bi_wand PROP Q H))) *)
| @typed_val_expr ?Σ ?tG ?e ?T => | @typed_val_expr ?Σ ?tG ?e ?T =>
li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_val_expr Σ tG e H))) 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 => | @typed_write ?Σ ?tG ?b ?e ?ot ?v ?ty ?Mov ?T =>
......
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