From 2131d528005f22c497a0c78e48d31ab32bf5296f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Oct 2017 15:14:42 +0200
Subject: [PATCH] use a section for local options
---
theories/base.v | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/theories/base.v b/theories/base.v
index cf4781b8..48a5fd0f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -18,11 +18,12 @@ Obligation Tactic := idtac.
Add Search Blacklist "_obligation_".
(** Sealing off definitions *)
-Set Primitive Projections.
-Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
-Arguments unseal {_ _} _ : assert.
-Arguments seal_eq {_ _} _ : assert.
-Unset Primitive Projections.
+Section seal.
+ Local Set Primitive Projections.
+ Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+ Arguments unseal {_ _} _ : assert.
+ Arguments seal_eq {_ _} _ : assert.
+End seal.
(** Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type
--
GitLab