From c60c51920e0f8f8e0595dedb55d25b3c9b6cf9c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2017 18:05:25 +0900
Subject: [PATCH] Add a constant `tc_opaque` for type class opaque definitions.

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

diff --git a/theories/base.v b/theories/base.v
index 0a0fd53c..cf4781b8 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -24,6 +24,13 @@ Arguments unseal {_ _} _ : assert.
 Arguments seal_eq {_ _} _ : assert.
 Unset Primitive Projections.
 
+(** Typeclass opaque definitions *)
+(* The constant [tc_opaque] is used to make definitions opaque for just type
+class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
+Definition tc_opaque {A} (x : A) : A := x.
+Typeclasses Opaque tc_opaque.
+Arguments tc_opaque {_} _ /.
+
 (* Below we define type class versions of the common logical operators. It is
 important to note that we duplicate the definitions, and do not declare the
 existing logical operators as type classes. That is, we do not say:
-- 
GitLab