Skip to content
Snippets Groups Projects

Enable `Hint Mode Equiv` now that stdpp requires Coq 8.12

Closed Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:mode-equiv into master
1 file
+ 2
2
Compare changes
  • Side-by-side
  • Inline
+ 2
2
@@ -270,8 +270,8 @@ Class Equiv A := equiv: relation A.
(* No Hint Mode set because of Coq bug #14441.
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
(** We instruct setoid rewriting to infer [equiv] as a relation on
type [A] when needed. This allows setoid_rewrite to solve constraints
of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
when an equivalence relation is available on type [A]. We put this instance
at level 150 so it does not take precedence over Coq's stdlib instances,
Loading