From 89e2c15397d51b3a6d238d402058c55a0695955b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 12 Aug 2020 16:46:22 +0200
Subject: [PATCH] do not eta-expand when sealing

---
 theories/algebra/ofe.v                    |  3 +-
 theories/base_logic/lib/fancy_updates.v   |  9 +++--
 theories/base_logic/lib/gen_heap.v        |  3 +-
 theories/base_logic/lib/invariants.v      |  4 +-
 theories/base_logic/lib/own.v             |  4 +-
 theories/base_logic/upred.v               | 45 +++++++++++++++--------
 theories/bi/big_op.v                      |  2 +-
 theories/bi/lib/atomic.v                  |  6 +--
 theories/bi/monpred.v                     | 39 ++++++++++++--------
 theories/program_logic/total_weakestpre.v | 14 ++++---
 theories/program_logic/weakestpre.v       | 13 ++++---
 theories/proofmode/environments.v         |  2 +
 12 files changed, 88 insertions(+), 56 deletions(-)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 71c86a043..db535df5d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -315,7 +315,8 @@ Qed.
 Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A)
   `{!Contractive f} : A := compl (fixpoint_chain f).
 Definition fixpoint_aux : seal (@fixpoint_def). Proof. by eexists. Qed.
-Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
+Definition fixpoint := fixpoint_aux.(unseal).
+Arguments fixpoint {A AC AiH} f {Hf} : rename.
 Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
 Section fixpoint.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 6cdf3d284..3334e0bcf 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -9,10 +9,11 @@ Import uPred.
 
 Definition uPred_fupd_def `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P).
-Definition uPred_fupd_aux `{!invG Σ} : seal uPred_fupd_def. Proof. by eexists. Qed.
-Definition uPred_fupd `{!invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
-Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
-  uPred_fupd_aux.(seal_eq).
+Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
+Definition uPred_fupd := uPred_fupd_aux.(unseal).
+Arguments uPred_fupd {_ _}.
+Definition uPred_fupd_eq `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
 Lemma uPred_fupd_mixin `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
 Proof.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 5eeff6cdb..2014cd67d 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -121,9 +121,10 @@ Section definitions.
     ∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
           own γm (namespace_map_data N (to_agree (encode x))).
   Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
-  Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
+  Definition meta := meta_aux.(unseal).
   Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
+Arguments meta {_ _ _ _ Σ _ _ _ _} l N x.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 9362abc84..c95573a02 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -10,10 +10,10 @@ Import uPred.
 Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   □ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True).
 Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
-Definition inv {Σ i} := inv_aux.(unseal) Σ i.
+Definition inv := inv_aux.(unseal).
+Arguments inv {Σ i} : rename.
 Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
 Instance: Params (@inv) 3 := {}.
-Typeclasses Opaque inv.
 
 (** * Invariants *)
 Section inv.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index ce5889435..79d83df86 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -58,10 +58,10 @@ Instance: Params (@iRes_singleton) 4 := {}.
 Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Definition own_aux : seal (@own_def). Proof. by eexists. Qed.
-Definition own {Σ A i} := own_aux.(unseal) Σ A i.
+Definition own := own_aux.(unseal).
+Arguments own {Σ A i} : rename.
 Definition own_eq : @own = @own_def := own_aux.(seal_eq).
 Instance: Params (@own) 4 := {}.
-Typeclasses Opaque own.
 
 (** * Properties about ghost ownership *)
 Section global.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b84f1a1dd..fe44e0323 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -193,7 +193,8 @@ Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
   {| uPred_holds n x := φ |}.
 Solve Obligations with done.
 Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
-Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
+Definition uPred_pure := uPred_pure_aux.(unseal).
+Arguments uPred_pure {M}.
 Definition uPred_pure_eq :
   @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
 
@@ -201,14 +202,16 @@ Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∧ Q n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
-Definition uPred_and {M} := uPred_and_aux.(unseal) M.
+Definition uPred_and := uPred_and_aux.(unseal).
+Arguments uPred_and {M}.
 Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
 
 Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∨ Q n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
-Definition uPred_or {M} := uPred_or_aux.(unseal) M.
+Definition uPred_or := uPred_or_aux.(unseal).
+Arguments uPred_or {M}.
 Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
 
 Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M :=
@@ -220,7 +223,8 @@ Next Obligation.
   eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc.
 Qed.
 Definition uPred_impl_aux : seal (@uPred_impl_def). Proof. by eexists. Qed.
-Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
+Definition uPred_impl := uPred_impl_aux.(unseal).
+Arguments uPred_impl {M}.
 Definition uPred_impl_eq :
   @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
 
@@ -228,7 +232,8 @@ Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∀ a, Ψ a n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
-Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
+Definition uPred_forall := uPred_forall_aux.(unseal).
+Arguments uPred_forall {M A}.
 Definition uPred_forall_eq :
   @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
 
@@ -236,14 +241,16 @@ Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∃ a, Ψ a n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
-Definition uPred_exist {M A} := uPred_exist_aux.(unseal) M A.
+Definition uPred_exist := uPred_exist_aux.(unseal).
+Arguments uPred_exist {M A}.
 Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
 
 Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M :=
   {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
 Solve Obligations with naive_solver eauto 2 using dist_le.
 Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
-Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
+Definition uPred_internal_eq := uPred_internal_eq_aux.(unseal).
+Arguments uPred_internal_eq {M A}.
 Definition uPred_internal_eq_eq:
   @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
 
@@ -255,7 +262,8 @@ Next Obligation.
   eapply dist_le, Hn. by rewrite Hy Hx assoc.
 Qed.
 Definition uPred_sep_aux : seal (@uPred_sep_def). Proof. by eexists. Qed.
-Definition uPred_sep {M} := uPred_sep_aux.(unseal) M.
+Definition uPred_sep := uPred_sep_aux.(unseal).
+Arguments uPred_sep {M}.
 Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
 
 Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
@@ -267,7 +275,8 @@ Next Obligation.
     eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
 Qed.
 Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
-Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
+Definition uPred_wand := uPred_wand_aux.(unseal).
+Arguments uPred_wand {M}.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
 
@@ -278,7 +287,8 @@ Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
 Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
-Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
+Definition uPred_plainly := uPred_plainly_aux.(unseal).
+Arguments uPred_plainly {M}.
 Definition uPred_plainly_eq :
   @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
 
@@ -286,7 +296,8 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Solve Obligations with naive_solver eauto using uPred_mono, cmra_core_monoN.
 Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
-Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
+Definition uPred_persistently := uPred_persistently_aux.(unseal).
+Arguments uPred_persistently {M}.
 Definition uPred_persistently_eq :
   @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
 
@@ -296,7 +307,8 @@ Next Obligation.
   intros M P [|n1] [|n2] x1 x2; eauto using uPred_mono, cmra_includedN_S with lia.
 Qed.
 Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
-Definition uPred_later {M} := uPred_later_aux.(unseal) M.
+Definition uPred_later := uPred_later_aux.(unseal).
+Arguments uPred_later {M}.
 Definition uPred_later_eq :
   @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
 
@@ -307,7 +319,8 @@ Next Obligation.
   exists (a' â‹… x2). by rewrite Hx(assoc op) Hx1.
 Qed.
 Definition uPred_ownM_aux : seal (@uPred_ownM_def). Proof. by eexists. Qed.
-Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
+Definition uPred_ownM := uPred_ownM_aux.(unseal).
+Arguments uPred_ownM {M}.
 Definition uPred_ownM_eq :
   @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
 
@@ -315,7 +328,8 @@ Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M :=
   {| uPred_holds n x := ✓{n} a |}.
 Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
 Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
-Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
+Definition uPred_cmra_valid := uPred_cmra_valid_aux.(unseal).
+Arguments uPred_cmra_valid {M A}.
 Definition uPred_cmra_valid_eq :
   @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
 
@@ -330,7 +344,8 @@ Next Obligation.
   eauto using uPred_mono, cmra_includedN_l.
 Qed.
 Definition uPred_bupd_aux : seal (@uPred_bupd_def). Proof. by eexists. Qed.
-Definition uPred_bupd {M} := uPred_bupd_aux.(unseal) M.
+Definition uPred_bupd := uPred_bupd_aux.(unseal).
+Arguments uPred_bupd {M}.
 Definition uPred_bupd_eq :
   @uPred_bupd = @uPred_bupd_def := uPred_bupd_aux.(seal_eq).
 
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index fdf1fe182..768a35757 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -57,7 +57,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
 Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
 Definition big_sepM2 := big_sepM2_aux.(unseal).
 Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
-Definition big_sepM2_eq : @big_sepM2 = @big_sepM2_def := big_sepM2_aux.(seal_eq).
+Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
 Instance: Params (@big_sepM2) 6 := {}.
 Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
   (big_sepM2 (λ k x1 x2, P) m1 m2) : bi_scope.
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 3e695fcff..817e5473b 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -88,9 +88,9 @@ End definition.
 
 (** Seal it *)
 Definition atomic_update_aux : seal (@atomic_update_def). Proof. by eexists. Qed.
-Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
-Definition atomic_update_eq :
-  @atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
+Definition atomic_update := atomic_update_aux.(unseal).
+Arguments atomic_update {_ _ _ _}.
+Definition atomic_update_eq : @atomic_update = _ := atomic_update_aux.(seal_eq).
 
 Arguments atomic_acc {PROP _ TA TB} Eo Ei _ _ _ _ : simpl never.
 Arguments atomic_update {PROP _ TA TB} Eo Ei _ _ _ : simpl never.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index ee70c6117..14c5d02d0 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -1,5 +1,6 @@
 From stdpp Require Import coPset.
 From iris.bi Require Import bi.
+Set Default Proof Using "Type".
 
 (** Definitions. *)
 Structure biIndex :=
@@ -125,9 +126,9 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
   MonPred (λ i, (∀ j, ⌜i ⊑ j⌝ → Φ j)%I) _.
 Next Obligation. solve_proper. Qed.
 
-Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
+Definition monPred_embed_def : Embed PROP monPred := λ (P : PROP), MonPred (λ _, P) _.
 Definition monPred_embed_aux : seal (@monPred_embed_def). Proof. by eexists. Qed.
-Definition monPred_embed : Embed PROP monPred := monPred_embed_aux.(unseal).
+Definition monPred_embed := monPred_embed_aux.(unseal).
 Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
 
 Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
@@ -742,10 +743,11 @@ Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objectiv
 Program Definition monPred_bupd_def `{BiBUpd PROP} (P : monPred) : monPred :=
   MonPred (λ i, |==> P i)%I _.
 Next Obligation. solve_proper. Qed.
-Definition monPred_bupd_aux `{BiBUpd PROP} : seal monPred_bupd_def. Proof. by eexists. Qed.
-Definition monPred_bupd `{BiBUpd PROP} : BUpd _ := monPred_bupd_aux.(unseal).
-Definition monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = _ :=
-  monPred_bupd_aux.(seal_eq).
+Definition monPred_bupd_aux : seal (@monPred_bupd_def). Proof. by eexists. Qed.
+Definition monPred_bupd := monPred_bupd_aux.(unseal).
+Arguments monPred_bupd {_}.
+Definition monPred_bupd_eq `{BiBUpd PROP} : @bupd _ monPred_bupd = monPred_bupd_def.
+Proof. rewrite -monPred_bupd_aux.(seal_eq) //. Qed.
 
 Lemma monPred_bupd_mixin `{BiBUpd PROP} : BiBUpdMixin monPredI monPred_bupd.
 Proof.
@@ -806,11 +808,13 @@ Proof. rewrite /bi_except_0. apply _. Qed.
 (** Internal equality *)
 Definition monPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : monPred :=
   MonPred (λ _, a ≡ b)%I _.
-Definition monPred_internal_eq_aux `{!BiInternalEq PROP} : seal (@monPred_internal_eq_def _).
+Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def).
 Proof. by eexists. Qed.
-Definition monPred_internal_eq `{!BiInternalEq PROP} := monPred_internal_eq_aux.(unseal).
+Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
+Arguments monPred_internal_eq {_}.
 Definition monPred_internal_eq_eq `{!BiInternalEq PROP} :
-  @internal_eq _ (@monPred_internal_eq _) = _ := monPred_internal_eq_aux.(seal_eq).
+  @internal_eq _ (@monPred_internal_eq _) = monPred_internal_eq_def.
+Proof. rewrite -monPred_internal_eq_aux.(seal_eq) //. Qed.
 
 Lemma monPred_internal_eq_mixin `{!BiInternalEq PROP} :
   BiInternalEqMixin monPredI (@monPred_internal_eq _).
@@ -860,10 +864,11 @@ Program Definition monPred_fupd_def `{BiFUpd PROP} (E1 E2 : coPset)
         (P : monPred) : monPred :=
   MonPred (λ i, |={E1,E2}=> P i)%I _.
 Next Obligation. solve_proper. Qed.
-Definition monPred_fupd_aux `{BiFUpd PROP} : seal monPred_fupd_def. Proof. by eexists. Qed.
-Definition monPred_fupd `{BiFUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
-Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = _ :=
-  monPred_fupd_aux.(seal_eq).
+Definition monPred_fupd_aux : seal (@monPred_fupd_def). Proof. by eexists. Qed.
+Definition monPred_fupd := monPred_fupd_aux.(unseal).
+Arguments monPred_fupd {_}.
+Definition monPred_fupd_eq `{BiFUpd PROP} : @fupd _ monPred_fupd = monPred_fupd_def.
+Proof. rewrite -monPred_fupd_aux.(seal_eq) //. Qed.
 
 Lemma monPred_fupd_mixin `{BiFUpd PROP} : BiFUpdMixin monPredI monPred_fupd.
 Proof.
@@ -897,9 +902,11 @@ Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
 (** Plainly *)
 Definition monPred_plainly_def `{BiPlainly PROP} P : monPred :=
   MonPred (λ _, ∀ i, ■ (P i))%I _.
-Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. Proof. by eexists. Qed.
-Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := monPred_plainly_aux.(unseal).
-Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := monPred_plainly_aux.(seal_eq).
+Definition monPred_plainly_aux : seal (@monPred_plainly_def). Proof. by eexists. Qed.
+Definition monPred_plainly := monPred_plainly_aux.(unseal).
+Arguments monPred_plainly {_}.
+Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = monPred_plainly_def.
+Proof. rewrite -monPred_plainly_aux.(seal_eq) //. Qed.
 
 Lemma monPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin monPredI monPred_plainly.
 Proof.
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 955235d00..380ef4f3c 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -57,12 +57,14 @@ Proof.
     rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
 Qed.
 
-Definition twp_def `{!irisG Λ Σ} (s : stuckness) (E : coPset)
-    (e : expr Λ) (Φ : val Λ → iProp Σ) :
-  iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
-Definition twp_aux `{!irisG Λ Σ} : seal (@twp_def Λ Σ _). Proof. by eexists. Qed.
-Instance twp' `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness := twp_aux.(unseal).
-Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _ := twp_aux.(seal_eq).
+Definition twp_def `{!irisG Λ Σ} : Twp Λ (iProp Σ) stuckness
+  := λ s E e Φ, bi_least_fixpoint (twp_pre' s) (E,e,Φ).
+Definition twp_aux : seal (@twp_def). Proof. by eexists. Qed.
+Definition twp' := twp_aux.(unseal).
+Arguments twp' {_ _ _}.
+Existing Instance twp'.
+Definition twp_eq `{!irisG Λ Σ} : twp = @twp_def Λ Σ _.
+Proof. rewrite -twp_aux.(seal_eq) //. Qed.
 
 Section twp.
 Context `{!irisG Λ Σ}.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index ec4ab9f47..916f502f1 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -44,11 +44,14 @@ Proof.
   repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
-Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
-  coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
-Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). Proof. by eexists. Qed.
-Instance wp' `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
-Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
+Definition wp_def `{!irisG Λ Σ} : Wp Λ (iProp Σ) stuckness :=
+  λ s : stuckness, fixpoint (wp_pre s).
+Definition wp_aux : seal (@wp_def). Proof. by eexists. Qed.
+Definition wp' := wp_aux.(unseal).
+Arguments wp' {_ _ _}.
+Existing Instance wp'.
+Definition wp_eq `{!irisG Λ Σ} : wp = @wp_def Λ Σ _.
+Proof. rewrite -wp_aux.(seal_eq) //. Qed.
 
 Section wp.
 Context `{!irisG Λ Σ}.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index e11fb4bce..ba7407827 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -257,6 +257,8 @@ Definition of_envs {PROP : bi} (Δ : envs PROP) : PROP :=
 Instance: Params (@of_envs) 1 := {}.
 Arguments of_envs : simpl never.
 
+(* FIXME this is not at all our usual sealing pattern.
+The [def] is missing and the [eq] doesn't even match the definition in [aux]! *)
 Definition envs_entails_aux :
   seal (λ (PROP : bi) (Γp Γs : env PROP) (Q : PROP), of_envs' Γp Γs ⊢ Q).
 Proof. by eexists. Qed.
-- 
GitLab