From 7746448fdbb583cc340822e46cbe6f94ed404e0c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Sep 2021 14:27:06 -0400
Subject: [PATCH] prepare for weaker f_equiv
---
theories/typing/lib/ghostcell.v | 4 ++--
theories/typing/own.v | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 6a5dc438..6ff1ae07 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -101,8 +101,8 @@ Section ghostcell.
Proof.
rewrite /Fractional=>q1 q2.
rewrite -own_op /ghosttoken_st_to_R /=. f_equiv.
- rewrite -Cinr_op. f_equiv.
- rewrite -pair_op. f_equiv.
+ rewrite -Cinr_op. eapply Cinr_proper.
+ rewrite -pair_op. f_equiv; [|done..].
rewrite agree_idemp. done.
Qed.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 20c253f3..05911b24 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -39,7 +39,7 @@ Section own.
- iSplit.
+ by iIntros "[[]?]".
+ by iIntros "[]".
- - rewrite heap_freeable_op_eq. f_equiv.
+ - rewrite heap_freeable_op_eq. f_equiv; [|done..].
by rewrite -Qp_div_add_distr pos_to_Qp_add -Nat2Pos.inj_add.
Qed.
--
GitLab