Commit e626f081 authored by Robbert Krebbers's avatar Robbert Krebbers

Change mode of `TCEq`.

parent 20ef8941
......@@ -146,14 +146,14 @@ Existing Instance TCElemOf_here.
Existing Instance TCElemOf_further.
Hint Mode TCElemOf ! ! ! : typeclass_instances.
(** Similarly to [TCForall2], we declare the modes of [TCEq x y] in both
directions, i.e., either [x] input and [y] output, or [y] input and [x]
output. *)
(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
[TCEq] can also be used to unify evars. This is harmless: since the only
instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See for a use case. *)
Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
Existing Instance TCEq_refl.
Hint Mode TCEq ! ! - : typeclass_instances.
Hint Mode TCEq ! - ! : typeclass_instances.
Hint Mode TCEq ! - - : typeclass_instances.
Inductive TCDiag {A} (C : A Prop) : A A Prop :=
| TCDiag_diag x : C x TCDiag C x x.
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