add RETURN_MARKER back

theories/typing/automation.v

@@ -181,7 +181,7 @@ Ltac liRIntroduceTypedStmt :=
         let HQ := fresh "Q" in
         let HR := fresh "R" in
         pose (HQ := (CODE_MARKER Q));
-        pose (HR := (LET_ID R));
+        pose (HR := (RETURN_MARKER 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,6 +21,11 @@ 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 :=
@@ -92,6 +97,7 @@ 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 ::=