perf: replaced best tactics by hauto l: on

formal-land · Dec 16, 2024 · aa6ce05 · aa6ce05
1 parent 73adf52
commit aa6ce05
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -893,7 +893,7 @@ Proof.
     destruct p as [t0' type_safety_checker'].
     destruct t0'; cbn; trivial.
     unfold set; cbn.
-    best.
+    hauto l: on.
   }
   { guard_instruction Bytecode.Shr.
     unfold_state_monad.
@@ -914,7 +914,7 @@ Proof.
     destruct p as [t0' type_safety_checker'].
     destruct t0'; cbn; trivial.
     unfold set; cbn.
-    best.
+    hauto l: on.
   }
   { guard_instruction (Bytecode.VecPack t z).
     admit.