try old unfold

theories/lithium/interpreter.v

@@ -306,20 +306,29 @@ Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
        change_no_check G).
 
 Ltac liUnfoldLetGoal :=
-  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
+  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 :=