diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 54bab13e11fdd94aec4ad389bbf58d244137916c..e0f5fdde1f1a8f82a25f39a3a7d0a64e018235a6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -626,3 +626,5 @@ Proof.
   by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
 Qed.
 End classes.
+
+Hint Mode ProgIntoLaterN + - ! - : typeclass_instances.