Revert "add unfold_let_goal_tac"

This reverts commit 9159a9c7.

theories/lithium/interpreter.v

@@ -305,19 +305,28 @@ Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
        let G := tac H in
        change_no_check G).
 
-(* unfold_let_goal_tac lets users unfold custom definitions. *)
-Ltac unfold_let_goal_tac P := idtac.
 Ltac liUnfoldLetGoal :=
   match goal with
   | |- envs_entails _ ?P =>
       let h := get_head P in
       is_var P;
       unfold LET_ID in P;
-      unfold_let_goal_tac P;
-      (* This unfold inserts a cast but that is not too bad for
-      performance since the goal is small at this point. *)
       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

@@ -47,9 +47,6 @@ Ltac solve_protected_eq_unfold_tac ::=
   | |- _ => idtac
   end.
 
-Ltac unfold_let_goal_tac P :=
-  unfold RETURN_MARKER in P.
-
 Ltac can_solve_tac ::= solve_goal.
 
 Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.

theories/typing/automation/proof_state.v

@@ -23,6 +23,8 @@ Ltac unfold_code_marker_and_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 *)