From eebf68aaaedd1a02abafebebca3db75a57db9f48 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 30 Nov 2016 13:06:02 +0100
Subject: [PATCH] Use primitive projections for sealing

This approach is originally by Robbert
---
 theories/base.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 92606a94..e1c36a0a 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -14,6 +14,13 @@ Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 Obligation Tactic := idtac.
 
+(** Sealing off definitions *)
+Set Primitive Projections.
+Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+Arguments unseal {_ _} _.
+Arguments seal_eq {_ _} _.
+Unset Primitive Projections.
+
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.
-- 
GitLab