Commit 61180d3e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Useless parameter.

parent 82945e24
Pipeline #64833 passed with stages
in 23 seconds
......@@ -28,7 +28,7 @@ Class Decidable (P : Prop) := decide : {P} + {~P}.
Arguments decide _ {_}.
(** A [Comparable] type has decidable equality. *)
Instance comparable_decidable_eq T `{Comparable T, ComparableUsualEq T} (x y : T) :
Instance comparable_decidable_eq T `{ComparableUsualEq T} (x y : T) :
Decidable (x = y).
Proof.
unfold Decidable.
......
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