From c8d58d4caa54d1dc8eb8f24933de5564e9689559 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 2 Feb 2018 13:40:26 +0100
Subject: [PATCH] Type class version of equality.

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

diff --git a/theories/base.v b/theories/base.v
index 61d2b69a..5cd1bd9b 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -99,6 +99,10 @@ Existing Class TCForall2.
 Existing Instance TCForall2_nil.
 Existing Instance TCForall2_cons.
 
+Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
+Existing Class TCEq.
+Existing Instance TCEq_refl.
+
 (** 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