Skip to content
Snippets Groups Projects
Commit 9fddc01a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Set `Hint Mode` for `Equiv`.

parent 8574b623
No related branches found
No related tags found
1 merge request!473Take advantage of new Coq features in Coq 8.15
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 2 deletions
stdpp/base.v
+ 1
− 2
View file @ 9fddc01a
......@@ -265,8 +265,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 bug #14441.
Global Hint Mode Equiv ! : typeclass_instances. *)
Global Hint Mode Equiv ! : typeclass_instances.
(** We instruct setoid rewriting to infer [equiv] as a relation on
type [A] when needed. This allows setoid_rewrite to solve constraints
......
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