perf: replaced best tactics by hauto drew: off

formal-land · Dec 17, 2024 · a7e5857 · a7e5857
1 parent 1137b0d
commit a7e5857
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
@@ -709,7 +709,7 @@ Proof.
     destruct AbstractStack.pop as [[operand stack']|]; cbn; [|trivial].
     unfold set; cbn.
     repeat(step; cbn; trivial).
-    best.
+    hauto drew: off.
   }
   { guard_instruction (Bytecode.Call t).
     admit.