From 9652b7b3512efdfd5bce777f88138d71f0e9c9ab Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 22 Jan 2017 13:00:09 +0100
Subject: [PATCH] Hint Mode for auxilary proof mode class ProgIntoLaterN.
---
theories/proofmode/class_instances.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 54bab13e1..e0f5fdde1 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.
--
GitLab