add unfold_let_goal_tac

theories/lithium/interpreter.v

@@ -305,28 +305,19 @@ 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 H := idtac.
 Ltac liUnfoldLetGoal :=
   match goal with
   | |- envs_entails _ ?P =>
       let H := get_head P in
       is_var H;
       unfold LET_ID in H;
+      unfold_let_goal_tac H;
+      (* This unfold inserts a cast but that is not too bad for
+      performance since the goal is small at this point. *)
       unfold H;
       try clear H
-  (* 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,6 +47,9 @@ Ltac solve_protected_eq_unfold_tac ::=
   | |- _ => idtac
   end.
 
+Ltac unfold_let_goal_tac H :=
+  unfold RETURN_MARKER in H.
+
 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,8 +23,6 @@ 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 *)