From a5063f60b461e099a5b029dd0c2ae43e8e45e43e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Aug 2017 22:30:47 +0200
Subject: [PATCH] Enable primitive projections for bi.interface.
This gives a 25% speedup on some files (e.g. boxes).
This commit contains some hacks to work arround Coq issue #5699.
This commit requires Coq v8.7 together with
https://github.com/coq/coq/pull/1006
---
opam | 2 +-
theories/base_logic/upred.v | 15 +++++++--------
theories/bi/interface.v | 1 +
3 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/opam b/opam
index 84f0313fb..d68224567 100644
--- a/opam
+++ b/opam
@@ -10,6 +10,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
- "coq" { >= "8.7.0" & < "8.8~" }
+ "coq" { >= "8.7.dev" & < "8.8~" }
"coq-stdpp" { (= "dev.2017-11-12.2") | (= "dev") }
]
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 094577409..3551b7dfa 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -324,14 +324,13 @@ Definition unseal_eqs :=
uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_plainly_eq, uPred_persistently_eq, uPred_later_eq, uPred_ownM_eq,
uPred_cmra_valid_eq, uPred_bupd_eq).
-Ltac unseal := rewrite
- /bi_emp /= /uPred_emp /bi_pure /bi_and /bi_or /bi_impl
- /bi_forall /bi_exist /bi_internal_eq /bi_sep /bi_wand /bi_plainly
- /bi_persistently /bi_later /=
- /sbi_emp /sbi_pure /sbi_and /sbi_or /sbi_impl
- /sbi_forall /sbi_exist /sbi_internal_eq /sbi_sep /sbi_wand /sbi_plainly
- /sbi_persistently /=
- !unseal_eqs /=.
+Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+ unfold bi_emp; simpl;
+ unfold uPred_emp, bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+ bi_internal_eq, bi_sep, bi_wand, bi_plainly, bi_persistently, bi_later; simpl;
+ unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
+ sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl;
+ rewrite !unseal_eqs /=.
End uPred_unseal.
Import uPred_unseal.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ed0851fd9..44c05c3f1 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,4 +1,5 @@
From iris.algebra Require Export ofe.
+Set Primitive Projections.
Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "'emp'".
--
GitLab