fix

theories/lithium/interpreter.v

@@ -308,11 +308,11 @@ Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
 Ltac liUnfoldLetGoal :=
   match goal with
   | |- envs_entails _ ?P =>
-      let h := get_head P in
-      is_var P;
-      unfold LET_ID in P;
-      unfold P;
-      try clear P
+      let H := get_head P in
+      is_var H;
+      unfold LET_ID in H;
+      unfold H;
+      try clear H
   (* lazymatch goal with *)
   (* | |- envs_entails ?Δ ?P => *)
   (*     let h := get_head P in *)