From 4c60de243e83372f2907f1315ddbdf9ae1f70956 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 01:57:19 +0100
Subject: [PATCH] Add `TCDiag` type class.

---
 theories/base.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 81022e4e..c0733e1f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -133,6 +133,11 @@ Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
 Existing Instance TCEq_refl.
 
+Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
+  | TCDiag_diag x : C x → TCDiag C x x.
+Existing Class TCDiag.
+Existing Instance TCDiag_diag.
+
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope stdpp_scope with stdpp.
-- 
GitLab