diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index f5eea3e90df1d57f8db150b4ce8445d62e4b841a..81d0a3e5e93100d0ae0e22484b64a4f2f151e401 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -680,7 +680,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
           fail "iSpecialize:" H "not found"
          |iSpecializePat H pat;
            [..
-           |refine (tac_specialize_persistent_helper_done _ H _ _ _);
+           |notypeclasses refine (tac_specialize_persistent_helper_done _ H _ _ _);
             pm_reflexivity]
          |iSolveTC ||
           let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in