Commit 9652b7b3 authored by Robbert Krebbers's avatar Robbert Krebbers

Hint Mode for auxilary proof mode class ProgIntoLaterN.

parent da3aa7e4
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment