Skip to content
Snippets Groups Projects
Commit edb87363 authored by Pierre Courtieu's avatar Pierre Courtieu
Browse files

Typo.

parent ff0d0cb7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
Util/SetoidDefs.v
+ 1
− 1
View file @ edb87363
...@@ -29,7 +29,7 @@ Set Implicit Arguments. ...@@ -29,7 +29,7 @@ Set Implicit Arguments.
(* To avoid infinite loops, we use a breadth-first search... *) (* To avoid infinite loops, we use a breadth-first search... *)
Typeclasses eauto := (bfs) 20. Typeclasses eauto := (bfs) 20.
(* but we need to remove [eq_setoid] as it matches everything... *) (* but we need to remove [eq_setoid] as it matches everything... *)
Remove Hints eq_setoid : Setoid. Global Remove Hints eq_setoid : Setoid.
(* while still declaring it for the types for which we still want to use it. *) (* while still declaring it for the types for which we still want to use it. *)
Instance R_Setoid : Setoid R := eq_setoid R. Instance R_Setoid : Setoid R := eq_setoid R.
Instance Z_Setoid : Setoid Z := eq_setoid Z. Instance Z_Setoid : Setoid Z := eq_setoid Z.
......
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