different liUnfoldLetGoal

theories/lithium/interpreter.v

@@ -279,6 +279,7 @@ Ltac liEnforceInvariant :=
                 )
   end.
 
+(*
 Ltac liFresh :=
   lazymatch goal with
   | [ H := Envs _ _ ?n |- _ ] =>
@@ -295,16 +296,30 @@ Ltac liFresh :=
   end in
     constr:(IAnon n)
   end.
+ *)
+
+Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
+  try (assert_fails (is_var T);
+       let H := fresh "GOAL" in
+       pose H := (LET_ID T);
+       let G := tac H in
+       change_no_check G).
 
 Ltac liUnfoldLetGoal :=
-  match goal with
-  | |- envs_entails _ ?P =>
-    let rec go P tac :=
-        match P with
-        | ?Q ?R => go Q tac
-        | _ => is_var P; tac P
-        end in
-    go P ltac:(fun P => unfold LET_ID in P; unfold P; try clear P)
+  lazymatch goal with
+  | |- envs_entails ?Δ ?P =>
+      let h := get_head P in
+      is_var h;
+      let u := eval unfold h in h in
+        lazymatch u with
+        | LET_ID ?G =>
+            lazymatch P with
+            | context C [h] =>
+                let X := context C [G] in
+                change_no_check (envs_entails Δ G);
+                try clear h
+            end
+        end
   end.
 
 Ltac liUnfoldLetsInContext :=

theories/typing/automation.v

@@ -95,18 +95,17 @@ End automation.
 Ltac liRIntroduceLetInGoal :=
   lazymatch goal with
   | |- @envs_entails ?PROP ?Δ ?P =>
-    let H := fresh "GOAL" in
     lazymatch P with
     | @bi_wand ?PROP ?Q ?T =>
-      pose H := (LET_ID T); change_no_check (@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 =>
-      pose (H := LET_ID T); change_no_check (@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 =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_write Σ tG b e ot v ty Mov H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_write Σ tG b e ot v ty Mov H)))
     | @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H)))
     | @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H)))
     end
   end.