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 Δ X);
+                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.
 
@@ -181,7 +180,7 @@ Ltac liRIntroduceTypedStmt :=
         let HQ := fresh "Q" in
         let HR := fresh "R" in
         pose (HQ := (CODE_MARKER Q));
-        pose (HR := (RETURN_MARKER R));
+        pose (HR := (LET_ID R));
         change_no_check (@envs_entails PROP Δ (@typed_stmt Σ tG s fn ls HR HQ));
         iEval (simpl) (* To simplify f_init *)
       end

theories/typing/automation/proof_state.v

@@ -21,11 +21,6 @@ Arguments CODE_MARKER : simpl never.
 Ltac unfold_code_marker_and_compute_map_lookup :=
   unfold CODE_MARKER in *; compute_map_lookup.
 
-Definition RETURN_MARKER `{!typeG Σ} (R : val → mtype → iProp Σ) : val → mtype → iProp Σ := R.
-Notation "'HIDDEN'" := (RETURN_MARKER _) (only printing).
-(* simplify RETURN_MARKER as soon as it is applied enough in the goal *)
-Arguments RETURN_MARKER _ _ _ _ _ /.
-
 
 (** * Tactics for manipulating location information *)
 Ltac get_loc_info cont :=
@@ -97,7 +92,6 @@ Ltac prepare_sideconditions :=
   repeat match goal with | H : BLOCK_PRECOND _ _ |- _ => clear H end;
   (* get rid of Q *)
   repeat match goal with | H := CODE_MARKER _ |- _ => clear H end;
-  repeat match goal with | H := RETURN_MARKER _ |- _ => clear H end;
   clear_unused_vars.
 
 Ltac solve_goal_prepare_tac ::=