Commit e383889e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove Hint Mode that was already declared elsewhere (in classes.v).

parent 46b5387d
...@@ -707,5 +707,3 @@ Proof. ...@@ -707,5 +707,3 @@ Proof.
by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P). by rewrite -{2}HP -(except_0_idemp P) -except_0_bupd -(except_0_intro P).
Qed. Qed.
End classes. End classes.
Hint Mode IntoLaterN' + - ! - : 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