From 79877aadde02f9734d2b50cc8904d983e9dc4936 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Sep 2023 14:46:22 +0000
Subject: [PATCH] Revert "Merge branch 'janno/tc-opaque-unseal' into 'master'"
This reverts merge request !487
---
stdpp/base.v | 1 -
1 file changed, 1 deletion(-)
diff --git a/stdpp/base.v b/stdpp/base.v
index 29f1d074..4aaf0376 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -56,7 +56,6 @@ Add Search Blacklist "_unseal".
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
Global Arguments unseal {_ _} _ : assert.
Global Arguments seal_eq {_ _} _ : assert.
-Global Typeclasses Opaque unseal.
(** * Solving type class instances *)
(** The tactic [tc_solve] is used to solve type class goals by invoking type
--
GitLab