From 4ad2b78fff6ae67956ccd188ee0bb3e0793ccc10 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 14 Dec 2017 15:25:08 +0100
Subject: [PATCH] MonPred.unseal in a module.
---
theories/bi/monpred.v | 3 +++
1 file changed, 3 insertions(+)
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 45714544e..0f7a3ea09 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -208,6 +208,7 @@ Definition monPred_later_aux {I PROP} : seal (@monPred_later_def I PROP). by eex
Definition monPred_later {I PROP} := unseal (@monPred_later_aux I PROP).
Definition monPred_later_eq {I PROP} : @monPred_later I PROP = _ := seal_eq _.
+Module MonPred.
Definition unseal_eqs :=
(@monPred_and_eq, @monPred_or_eq, @monPred_impl_eq,
@monPred_forall_eq, @monPred_exist_eq, @monPred_internal_eq_eq,
@@ -224,6 +225,8 @@ Ltac unseal :=
bi_plainly; simpl;
unfold monPred_pure, monPred_emp, monPred_plainly; simpl;
rewrite !unseal_eqs /=.
+End MonPred.
+Import MonPred.
Section canonical_bi.
Context (I : bi_index) (PROP : bi).
--
GitLab