diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index f838bf02249f22bd8a5e01f2f62d1a89d7071314..038d0c74e6708525f1e1547503a7ae1976723f09 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -736,6 +736,12 @@ Tactic Notation "ospecialize" "*" uconstr(p) :=
       pose proof p as H'; clear H; rename H' into H
   )).
 
+(** Tactic that works like [notypeclasses refine] but automatically determines
+the right number of [_]. This is *not* goal-directed, it will add [_] until the
+given term is no longer a function type. *)
+Tactic Notation "notypeclasses" "apply" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p => notypeclasses refine p).
+
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)
 Definition block {A : Type} (a : A) := a.
diff --git a/stdpp_bitvector/definitions.v b/stdpp_bitvector/definitions.v
index af70961286cb48cc4ca2f3bd97377ac794941dca..36a1b7381ca5eb2aaa9ae2bce99e002131cf7ec7 100644
--- a/stdpp_bitvector/definitions.v
+++ b/stdpp_bitvector/definitions.v
@@ -755,7 +755,7 @@ Global Hint Resolve bv_wrap_simplify_mul | 10 : bv_wrap_simplify_db.
  tries to simplify them by removing any [bv_wrap] inside z1. *)
 Ltac bv_wrap_simplify_left :=
   lazymatch goal with |- bv_wrap _ _ = _ => idtac end;
-  etrans; [ notypeclasses refine (bv_wrap_simplify_proof _ _ _);
+  etrans; [ notypeclasses apply bv_wrap_simplify_proof;
             typeclasses eauto with bv_wrap_simplify_db | ]
 .
 
diff --git a/tests/tactics.ref b/tests/tactics.ref
index 8004020e70975cdfb901869c2183a3a77a3390ef..02a7792497a438687f53f93b2c9ba38674bb6931 100644
--- a/tests/tactics.ref
+++ b/tests/tactics.ref
@@ -65,5 +65,12 @@ use opose proof instead.
   H' : even n
   ============================
   even n
+"notypeclasses_apply_test"
+     : string
+1 goal
+  
+  n : nat
+  ============================
+  Decision (n = 0)
 The command has indeed failed with message:
 No such assumption.
diff --git a/tests/tactics.v b/tests/tactics.v
index 2e755290c691f7bff55d13cc26b7e2bf37b9c9bd..0df8646f8edaa48e21aa076d0f1697cb6840b06a 100644
--- a/tests/tactics.v
+++ b/tests/tactics.v
@@ -234,6 +234,12 @@ Proof.
   done.
 Qed.
 
+Check "notypeclasses_apply_test".
+Lemma notypeclasses_apply_test n : {n = 0} + {¬ n = 0}.
+Proof.
+  notypeclasses apply (@decide _). Show.
+Abort.
+
 (** Some tests for f_equiv. *)
 (* Similar to [f_equal], it should solve goals by [reflexivity]. *)
 Lemma test_f_equiv_refl {A} (R : relation A) `{!Equivalence R} x :