From 7e6a432ff331b37b7107f4eecccbc6f6b511b70f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Nov 2016 10:43:56 +0100
Subject: [PATCH] No longer make slice_name type classes opaque.

We need instances like EqDecision and Countable for it. We could
redeclare those instead, though.
---
 base_logic/lib/boxes.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/base_logic/lib/boxes.v b/base_logic/lib/boxes.v
index 6079a03e4..820a79e2d 100644
--- a/base_logic/lib/boxes.v
+++ b/base_logic/lib/boxes.v
@@ -197,4 +197,4 @@ Proof.
 Qed.
 End box.
 
-Typeclasses Opaque slice_name slice box.
+Typeclasses Opaque slice box.
-- 
GitLab