unfold less

theories/lithium/interpreter.v

@@ -320,6 +320,14 @@ Ltac liUnfoldLetGoal :=
       try clear H
   end.
 
+Ltac liUnfoldLetsContaining H :=
+  repeat match goal with
+       | Hx := context [ H ] |- _ =>
+                unfold LET_ID in Hx;
+                unfold Hx;
+                clear Hx
+       end.
+
 Ltac liUnfoldLetsInContext :=
   repeat match goal with
   | H := LET_ID _ |- _ => unfold LET_ID in H; unfold H; clear H
@@ -350,8 +358,7 @@ Ltac create_protected_evar A :=
 Ltac unfold_instantiated_evar_hook H := idtac.
 
 Ltac unfold_instantiated_evar H :=
-  (* Necessary because the lets might contain evars. *)
-  liUnfoldLetsInContext;
+  liUnfoldLetsContaining H;
   unfold_instantiated_evar_hook H;
   revert H;
   repeat match goal with
@@ -384,10 +391,9 @@ Ltac unfold_instantiated_evar H :=
   It can use _ to create new evars, but they should be surrounded by [protected (EVAR_ID _)] such that instantiate_protected can find them and create the right let bindings afterwards.
 *)
 Ltac instantiate_protected H' tac_with :=
-  (* Necessary because the lets might contain evars. *)
-  liUnfoldLetsInContext;
   lazymatch H' with
   | protected ?H =>
+    liUnfoldLetsContaining H;
     unfold EVAR_ID in H;
     (* we have to be vary careful how we instantiate the evar, as it
     may not rely on things introduced later (even let bindings),