Unfold instantiated evars on each liRStep.

theories/lithium/interpreter.v

@@ -235,7 +235,7 @@ Local Tactic Notation "liChangeState" hyp(H) constr(Δ) :=
     rename H' into H
   end.
 
-Tactic Notation "liEnforceInvariant" :=
+Ltac liEnforceInvariant :=
   lazymatch goal with
   | |- @envs_entails ?PROP ?Δ ?P =>
     let with_H tac :=
@@ -258,6 +258,7 @@ Tactic Notation "liEnforceInvariant" :=
                    change_no_check (envs_entails H P)
                 )
   end.
+
 Ltac liFresh :=
   lazymatch goal with
   | [ H : IPM_STATE ?n |- _ ] =>
@@ -385,6 +386,9 @@ Ltac solve_protected_eq :=
   try ( liUnfoldAllEvars; match goal with |- ?a = ?b => unify a b with typeclass_instances end );
   exact: eq_refl.
 
+Ltac liEnforceInvariantAndUnfoldInstantiatedEvars :=
+  unfold_instantiated_evars; try liEnforceInvariant.
+
 (** * Main lithium tactics *)
 Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
 Ltac convert_to_i2p P cont :=

theories/typing/automation.v

@@ -201,7 +201,7 @@ Ltac liRJudgement :=
 
 (* This does everything *)
 Ltac liRStep :=
- try liEnforceInvariant;
+ liEnforceInvariantAndUnfoldInstantiatedEvars;
  try liRIntroduceLetInGoal;
  first [
    liRInstantiateEvars (* must be before do_side_cond and do_extensible_judgement *)
@@ -247,7 +247,7 @@ Tactic Notation "start_function" constr(fnname) "(" simple_intropattern(x) ")" :
 
 Ltac liRSplitBlocksIntro :=
   repeat (
-      try liEnforceInvariant;
+      liEnforceInvariantAndUnfoldInstantiatedEvars;
       first [
           liSep
         | liWand