Skip to content
Snippets Groups Projects
Commit 29af30c2 authored by Ralf Jung's avatar Ralf Jung
Browse files

update 'Equiv' mode comment

parent 34796f9a
No related branches found
No related tags found
No related merge requests found
......@@ -247,8 +247,7 @@ Proof. split; repeat intro; congruence. Qed.
"canonical" equivalence for a type. The typeclass is tied to the \equiv
symbol. This is based on (Spitters/van der Weegen, 2011). *)
Class Equiv A := equiv: relation A.
(* No Hint Mode set because of Coq bugs #5735 and #9058, only
fixed in Coq >= 8.12.
(* No Hint Mode set because of Coq bug #14441.
Global Hint Mode Equiv ! : typeclass_instances. *)
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment