only one let binding

TODO: This branch is probably not a good idea since it recreates a lot
of let-bindings instead of sharing them.

theories/lithium/interpreter.v

@@ -298,12 +298,35 @@ Ltac liFresh :=
   end.
  *)
 
-Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
-  try (assert_fails (is_var T);
-       let H := fresh "GOAL" in
+Ltac li_let_bind T tac :=
+  try lazymatch goal with | H := LET_ID _ |- _ => clear H end;
+  tryif is_var T then idtac else
+       let H := fresh "CONT" in
+       lazymatch goal with
+       | HL := LET_ID ?X |- _ =>
+           pose H := T;
+           let G := tac H in
+           change_no_check G;
+           revert HL H;
+           lazymatch goal with
+           | |- let H1 := ?X1 in let H2 := ?X2 in ?G =>
+               change (let H2 := LET_ID (let H1 := X1 in X2) in G);
+               intros H2
+           end
+       | _ =>
            pose H := (LET_ID T);
            let G := tac H in
-       change_no_check G).
+           change_no_check G
+       end.
+(* Ltac do_li_let_bind T 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). *)
+
+Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
+  li_let_bind T tac.
 
 (* unfold_let_goal_tac lets users unfold custom definitions. *)
 Ltac unfold_let_goal_tac H := idtac.
@@ -311,17 +334,45 @@ Ltac liUnfoldLetGoal :=
   let do_unfold P :=
     let H := get_head P in
     is_var H;
+    first [
+      lazymatch goal with
+      | H' := LET_ID (let X := ?A in ?B) |- _ =>
+          constr_eq H H';
+          revert H';
+          lazymatch goal with
+          | |- let H' := LET_ID (let X := ?A in ?B) in ?G =>
+            change (let X := A in let H' := B in G);
+            intros ?
+          end;
+          cbv zeta
+      end |
       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
+    ]
   in
   lazymatch goal with
   | |- envs_entails _ (?P ∗ _) => do_unfold P
   | |- envs_entails _ ?P => do_unfold P
   end.
+(* Ltac liUnfoldLetGoal := *)
+(*   let do_unfold 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 *)
+(*   in *)
+(*   lazymatch goal with *)
+(*   | |- envs_entails _ (?P ∗ _) => do_unfold P *)
+(*   | |- envs_entails _ ?P => do_unfold P *)
+(*   end. *)
 
 Ltac liUnfoldLetsContaining H :=
   repeat match goal with