1 files changed, 2 insertions, 2 deletions
diff --git a/src/QInst.v b/src/QInst.v
index 26430f1..b2dd836 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -27,7 +27,7 @@ Proof.
    installed when we compile SMTCoq. *)
 Qed.
 
-Hint Resolve impl_split.
+Hint Resolve impl_split : smtcoq_core.
 
 (** verit silently transforms an <implb (a || b) c> into a <or (not a) c>
    or into a <or (not b) c> when instantiating such a quantified theorem *)
@@ -208,7 +208,7 @@ Ltac vauto :=
                end
              ]
       );
-  auto.
+  auto with smtcoq_core.