sealing: Use primitive projection notation introduced in Coq master

This is backwards-compatible; it desugars to a normal application on previous versions

theories/algebra/ofe.v

@@ -300,8 +300,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). by eexists. Qed.
-Definition fixpoint {A AC AiH} f {Hf} := unseal fixpoint_aux A AC AiH f Hf.
-Definition fixpoint_eq : @fixpoint = @fixpoint_def := seal_eq fixpoint_aux.
+Definition fixpoint {A AC AiH} f {Hf} := fixpoint_aux.(unseal) A AC AiH f Hf.
+Definition fixpoint_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
 Section fixpoint.
   Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.

theories/base_logic/lib/fancy_updates.v

@@ -9,9 +9,9 @@ Import uPred.
 Definition uPred_fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
 Definition uPred_fupd_aux `{invG Σ} : seal uPred_fupd_def. by eexists. Qed.
-Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= unseal uPred_fupd_aux.
+Definition uPred_fupd `{invG Σ} : FUpd (iProp Σ):= uPred_fupd_aux.(unseal).
 Definition uPred_fupd_eq `{invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def :=
-  seal_eq uPred_fupd_aux.
+  uPred_fupd_aux.(seal_eq).
 
 Lemma uPred_fupd_mixin `{invG Σ} : BiFUpdMixin (uPredSI (iResUR Σ)) uPred_fupd.
 Proof.

theories/base_logic/lib/gen_heap.v

@@ -36,8 +36,8 @@ Section definitions.
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
     own (gen_heap_name hG) (◯ {[ l := (q, to_agree (v : leibnizC V)) ]}).
   Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
-  Definition mapsto := unseal mapsto_aux.
-  Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
+  Definition mapsto := mapsto_aux.(unseal).
+  Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
 End definitions.
 
 Local Notation "l ↦{ q } v" := (mapsto l q v)

theories/base_logic/lib/invariants.v

@@ -10,8 +10,8 @@ Import uPred.
 Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   (∃ i P', ⌜i ∈ (↑N:coPset)⌝ ∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I.
 Definition inv_aux : seal (@inv_def). by eexists. Qed.
-Definition inv {Σ i} := unseal inv_aux Σ i.
-Definition inv_eq : @inv = @inv_def := seal_eq inv_aux.
+Definition inv {Σ i} := inv_aux.(unseal) Σ i.
+Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
 Instance: Params (@inv) 3.
 Typeclasses Opaque inv.
 

theories/base_logic/lib/own.v

@@ -54,8 +54,8 @@ 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). by eexists. Qed.
-Definition own {Σ A i} := unseal own_aux Σ A i.
-Definition own_eq : @own = @own_def := seal_eq own_aux.
+Definition own {Σ A i} := own_aux.(unseal) Σ A i.
+Definition own_eq : @own = @own_def := own_aux.(seal_eq).
 Instance: Params (@own) 4.
 Typeclasses Opaque own.
 

theories/base_logic/upred.v

@@ -195,9 +195,9 @@ 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). by eexists. Qed.
-Definition uPred_pure {M} := unseal uPred_pure_aux M.
+Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
 Definition uPred_pure_eq :
-  @uPred_pure = @uPred_pure_def := seal_eq uPred_pure_aux.
+  @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
 
 Definition uPred_emp {M} : uPred M := uPred_pure True.
 
@@ -205,15 +205,15 @@ 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). by eexists. Qed.
-Definition uPred_and {M} := unseal uPred_and_aux M.
-Definition uPred_and_eq: @uPred_and = @uPred_and_def := seal_eq uPred_and_aux.
+Definition uPred_and {M} := uPred_and_aux.(unseal) 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). by eexists. Qed.
-Definition uPred_or {M} := unseal uPred_or_aux M.
-Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux.
+Definition uPred_or {M} := uPred_or_aux.(unseal) 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 :=
   {| uPred_holds n x := ∀ n' x',
@@ -224,32 +224,32 @@ Next Obligation.
   eapply HPQ; auto. exists (x2 ⋅ x4); by rewrite assoc.
 Qed.
 Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. Qed.
-Definition uPred_impl {M} := unseal uPred_impl_aux M.
+Definition uPred_impl {M} := uPred_impl_aux.(unseal) M.
 Definition uPred_impl_eq :
-  @uPred_impl = @uPred_impl_def := seal_eq uPred_impl_aux.
+  @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
 
 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). by eexists. Qed.
-Definition uPred_forall {M A} := unseal uPred_forall_aux M A.
+Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
 Definition uPred_forall_eq :
-  @uPred_forall = @uPred_forall_def := seal_eq uPred_forall_aux.
+  @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
 
 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). by eexists. Qed.
-Definition uPred_exist {M A} := unseal uPred_exist_aux M A.
-Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := seal_eq uPred_exist_aux.
+Definition uPred_exist {M A} := uPred_exist_aux.(unseal) 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 (A:=A)).
 Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). by eexists. Qed.
-Definition uPred_internal_eq {M A} := unseal uPred_internal_eq_aux M A.
+Definition uPred_internal_eq {M A} := uPred_internal_eq_aux.(unseal) M A.
 Definition uPred_internal_eq_eq:
-  @uPred_internal_eq = @uPred_internal_eq_def := seal_eq uPred_internal_eq_aux.
+  @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
 
 Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
@@ -259,8 +259,8 @@ Next Obligation.
   eapply dist_le, Hn. by rewrite Hy Hx assoc.
 Qed.
 Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed.
-Definition uPred_sep {M} := unseal uPred_sep_aux M.
-Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := seal_eq uPred_sep_aux.
+Definition uPred_sep {M} := uPred_sep_aux.(unseal) 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 :=
   {| uPred_holds n x := ∀ n' x',
@@ -271,9 +271,9 @@ Next Obligation.
     eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
 Qed.
 Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. Qed.
-Definition uPred_wand {M} := unseal uPred_wand_aux M.
+Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
 Definition uPred_wand_eq :
-  @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux.
+  @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
 
 (* Equivalently, this could be `∀ y, P n y`.  That's closer to the intuition
    of "embedding the step-indexed logic in Iris", but the two are equivalent
@@ -281,10 +281,10 @@ Definition uPred_wand_eq :
 Program Definition uPred_plainly_def {M} : Plainly (uPred M) := λ P,
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
-Definition uPred_plainly_aux {M} : seal (@uPred_plainly_def M). by eexists. Qed.
-Definition uPred_plainly {M} := unseal (@uPred_plainly_aux M).
-Definition uPred_plainly_eq M :
-  @plainly _ uPred_plainly = @uPred_plainly_def M := seal_eq uPred_plainly_aux.
+Definition uPred_plainly_aux : seal (@uPred_plainly_def). by eexists. Qed.
+Definition uPred_plainly {M} := uPred_plainly_aux.(unseal) M.
+Definition uPred_plainly_eq :
+  @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
 
 Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
@@ -292,9 +292,9 @@ Next Obligation.
   intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
 Qed.
 Definition uPred_persistently_aux : seal (@uPred_persistently_def). by eexists. Qed.
-Definition uPred_persistently {M} := unseal uPred_persistently_aux M.
+Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
 Definition uPred_persistently_eq :
-  @uPred_persistently = @uPred_persistently_def := seal_eq uPred_persistently_aux.
+  @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
 
 Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
   {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
@@ -302,9 +302,9 @@ 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). by eexists. Qed.
-Definition uPred_later {M} := unseal uPred_later_aux M.
+Definition uPred_later {M} := uPred_later_aux.(unseal) M.
 Definition uPred_later_eq :
-  @uPred_later = @uPred_later_def := seal_eq uPred_later_aux.
+  @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
 
 Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
   {| uPred_holds n x := a ≼{n} x |}.
@@ -313,17 +313,17 @@ Next Obligation.
   exists (a' ⋅ x2). by rewrite Hx(assoc op) Hx1.
 Qed.
 Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed.
-Definition uPred_ownM {M} := unseal uPred_ownM_aux M.
+Definition uPred_ownM {M} := uPred_ownM_aux.(unseal) M.
 Definition uPred_ownM_eq :
-  @uPred_ownM = @uPred_ownM_def := seal_eq uPred_ownM_aux.
+  @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
 
 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). by eexists. Qed.
-Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A.
+Definition uPred_cmra_valid {M A} := uPred_cmra_valid_aux.(unseal) M A.
 Definition uPred_cmra_valid_eq :
-  @uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux.
+  @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
 
 Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ k yf,
@@ -336,9 +336,9 @@ Next Obligation.
   eauto using uPred_mono, cmra_includedN_l.
 Qed.
 Definition uPred_bupd_aux {M} : seal (@uPred_bupd_def M). by eexists. Qed.
-Definition uPred_bupd {M} : BUpd (uPred M) := unseal uPred_bupd_aux.
+Definition uPred_bupd {M} : BUpd (uPred M) := uPred_bupd_aux.(unseal).
 Definition uPred_bupd_eq {M} :
-  @bupd _ uPred_bupd = @uPred_bupd_def M := seal_eq uPred_bupd_aux.
+  @bupd _ uPred_bupd = @uPred_bupd_def M := uPred_bupd_aux.(seal_eq).
 
 Module uPred_unseal.
 Definition unseal_eqs :=
@@ -352,6 +352,7 @@ Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
   bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_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_persistently; simpl;
+  unfold plainly, bi_plainly_plainly; simpl;
   rewrite !unseal_eqs /=.
 End uPred_unseal.
 Import uPred_unseal.

theories/bi/monpred.v

@@ -127,89 +127,89 @@ Next Obligation. solve_proper. Qed.
 
 Definition monPred_embed_def (P : PROP) : monPred := MonPred (λ _, P) _.
 Definition monPred_embed_aux : seal (@monPred_embed_def). by eexists. Qed.
-Definition monPred_embed : Embed PROP monPred := unseal monPred_embed_aux.
-Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := seal_eq _.
+Definition monPred_embed : Embed PROP monPred := monPred_embed_aux.(unseal).
+Definition monPred_embed_eq : @embed _ _ monPred_embed = _ := monPred_embed_aux.(seal_eq).
 
 Definition monPred_emp_def : monPred := MonPred (λ _, emp)%I _.
 Definition monPred_emp_aux : seal (@monPred_emp_def). by eexists. Qed.
-Definition monPred_emp := unseal monPred_emp_aux.
-Definition monPred_emp_eq : @monPred_emp = _ := seal_eq _.
+Definition monPred_emp := monPred_emp_aux.(unseal).
+Definition monPred_emp_eq : @monPred_emp = _ := monPred_emp_aux.(seal_eq).
 
 Definition monPred_pure_def (φ : Prop) : monPred := MonPred (λ _, ⌜φ⌝)%I _.
 Definition monPred_pure_aux : seal (@monPred_pure_def). by eexists. Qed.
-Definition monPred_pure := unseal monPred_pure_aux.
-Definition monPred_pure_eq : @monPred_pure = _ := seal_eq _.
+Definition monPred_pure := monPred_pure_aux.(unseal).
+Definition monPred_pure_eq : @monPred_pure = _ := monPred_pure_aux.(seal_eq).
 
 Definition monPred_objectively_def P : monPred := MonPred (λ _, ∀ i, P i)%I _.
 Definition monPred_objectively_aux : seal (@monPred_objectively_def). by eexists. Qed.
-Definition monPred_objectively := unseal monPred_objectively_aux.
-Definition monPred_objectively_eq : @monPred_objectively = _ := seal_eq _.
+Definition monPred_objectively := monPred_objectively_aux.(unseal).
+Definition monPred_objectively_eq : @monPred_objectively = _ := monPred_objectively_aux.(seal_eq).
 
 Definition monPred_subjectively_def P : monPred := MonPred (λ _, ∃ i, P i)%I _.
 Definition monPred_subjectively_aux : seal (@monPred_subjectively_def). by eexists. Qed.
-Definition monPred_subjectively := unseal monPred_subjectively_aux.
-Definition monPred_subjectively_eq : @monPred_subjectively = _ := seal_eq _.
+Definition monPred_subjectively := monPred_subjectively_aux.(unseal).
+Definition monPred_subjectively_eq : @monPred_subjectively = _ := monPred_subjectively_aux.(seal_eq).
 
 Program Definition monPred_and_def P Q : monPred :=
   MonPred (λ i, P i ∧ Q i)%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_and_aux : seal (@monPred_and_def). by eexists. Qed.
-Definition monPred_and := unseal (@monPred_and_aux).
-Definition monPred_and_eq : @monPred_and = _ := seal_eq _.
+Definition monPred_and := monPred_and_aux.(unseal).
+Definition monPred_and_eq : @monPred_and = _ := monPred_and_aux.(seal_eq).
 
 Program Definition monPred_or_def P Q : monPred :=
   MonPred (λ i, P i ∨ Q i)%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_or_aux : seal (@monPred_or_def). by eexists. Qed.
-Definition monPred_or := unseal (@monPred_or_aux).
-Definition monPred_or_eq : @monPred_or = _ := seal_eq _.
+Definition monPred_or := monPred_or_aux.(unseal).
+Definition monPred_or_eq : @monPred_or = _ := monPred_or_aux.(seal_eq).
 
 Definition monPred_impl_def P Q : monPred :=
   monPred_upclosed (λ i, P i → Q i)%I.
 Definition monPred_impl_aux : seal (@monPred_impl_def). by eexists. Qed.
-Definition monPred_impl := unseal (@monPred_impl_aux).
-Definition monPred_impl_eq : @monPred_impl = _ := seal_eq _.
+Definition monPred_impl := monPred_impl_aux.(unseal).
+Definition monPred_impl_eq : @monPred_impl = _ := monPred_impl_aux.(seal_eq).
 
 Program Definition monPred_forall_def A (Φ : A → monPred) : monPred :=
   MonPred (λ i, ∀ x : A, Φ x i)%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_forall_aux : seal (@monPred_forall_def). by eexists. Qed.
-Definition monPred_forall := unseal (@monPred_forall_aux).
-Definition monPred_forall_eq : @monPred_forall = _ := seal_eq _.
+Definition monPred_forall := monPred_forall_aux.(unseal).
+Definition monPred_forall_eq : @monPred_forall = _ := monPred_forall_aux.(seal_eq).
 
 Program Definition monPred_exist_def A (Φ : A → monPred) : monPred :=
   MonPred (λ i, ∃ x : A, Φ x i)%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_exist_aux : seal (@monPred_exist_def). by eexists. Qed.
-Definition monPred_exist := unseal (@monPred_exist_aux).
-Definition monPred_exist_eq : @monPred_exist = _ := seal_eq _.
+Definition monPred_exist := monPred_exist_aux.(unseal).
+Definition monPred_exist_eq : @monPred_exist = _ := monPred_exist_aux.(seal_eq).
 
 Program Definition monPred_sep_def P Q : monPred :=
   MonPred (λ i, P i ∗ Q i)%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_sep_aux : seal (@monPred_sep_def). by eexists. Qed.
-Definition monPred_sep := unseal monPred_sep_aux.
-Definition monPred_sep_eq : @monPred_sep = _ := seal_eq _.
+Definition monPred_sep := monPred_sep_aux.(unseal).
+Definition monPred_sep_eq : @monPred_sep = _ := monPred_sep_aux.(seal_eq).
 
 Definition monPred_wand_def P Q : monPred :=
   monPred_upclosed (λ i, P i -∗ Q i)%I.
 Definition monPred_wand_aux : seal (@monPred_wand_def). by eexists. Qed.
-Definition monPred_wand := unseal monPred_wand_aux.
-Definition monPred_wand_eq : @monPred_wand = _ := seal_eq _.
+Definition monPred_wand := monPred_wand_aux.(unseal).
+Definition monPred_wand_eq : @monPred_wand = _ := monPred_wand_aux.(seal_eq).
 
 Program Definition monPred_persistently_def P : monPred :=
   MonPred (λ i, <pers> (P i))%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_persistently_aux : seal (@monPred_persistently_def). by eexists. Qed.
-Definition monPred_persistently := unseal monPred_persistently_aux.
-Definition monPred_persistently_eq : @monPred_persistently = _ := seal_eq _.
+Definition monPred_persistently := monPred_persistently_aux.(unseal).
+Definition monPred_persistently_eq : @monPred_persistently = _ := monPred_persistently_aux.(seal_eq).
 
 Program Definition monPred_in_def (i0 : I) : monPred :=
   MonPred (λ i : I, ⌜i0 ⊑ i⌝%I) _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_in_aux : seal (@monPred_in_def). by eexists. Qed.
-Definition monPred_in := unseal (@monPred_in_aux).
-Definition monPred_in_eq : @monPred_in = _ := seal_eq _.
+Definition monPred_in := monPred_in_aux.(unseal).
+Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
 
 Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
   (* monPred_upclosed is not actually needed, since bupd is always
@@ -218,8 +218,8 @@ Definition monPred_bupd_def `{BUpd PROP} (P : monPred) : monPred :=
      terms in logical terms. *)
   monPred_upclosed (λ i, |==> P i)%I.
 Definition monPred_bupd_aux `{BUpd PROP} : seal monPred_bupd_def. by eexists. Qed.
-Definition monPred_bupd `{BUpd PROP} : BUpd _ := unseal monPred_bupd_aux.
-Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := seal_eq _.
+Definition monPred_bupd `{BUpd PROP} : BUpd _ := monPred_bupd_aux.(unseal).
+Definition monPred_bupd_eq `{BUpd PROP} : @bupd _ monPred_bupd = _ := monPred_bupd_aux.(seal_eq).
 End Bi.
 
 Arguments monPred_objectively {_ _} _%I.
@@ -235,19 +235,19 @@ Implicit Types P Q : monPred.
 
 Definition monPred_plainly_def `{BiPlainly PROP} P : monPred := MonPred (λ _, ∀ i, ■ (P i))%I _.
 Definition monPred_plainly_aux `{BiPlainly PROP} : seal monPred_plainly_def. by eexists. Qed.
-Definition monPred_plainly `{BiPlainly PROP} : Plainly _ := unseal monPred_plainly_aux.
-Definition monPred_plainly_eq `{BiPlainly PROP} : @plainly _ monPred_plainly = _ := seal_eq _.
+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_internal_eq_def (A : ofeT) (a b : A) : monPred := MonPred (λ _, a ≡ b)%I _.
 Definition monPred_internal_eq_aux : seal (@monPred_internal_eq_def). by eexists. Qed.
-Definition monPred_internal_eq := unseal monPred_internal_eq_aux.
-Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := seal_eq _.
+Definition monPred_internal_eq := monPred_internal_eq_aux.(unseal).
+Definition monPred_internal_eq_eq : @monPred_internal_eq = _ := monPred_internal_eq_aux.(seal_eq).
 
 Program Definition monPred_later_def P : monPred := MonPred (λ i, ▷ (P i))%I _.
 Next Obligation. solve_proper. Qed.
 Definition monPred_later_aux : seal monPred_later_def. by eexists. Qed.
-Definition monPred_later := unseal monPred_later_aux.
-Definition monPred_later_eq : monPred_later = _ := seal_eq _.
+Definition monPred_later := monPred_later_aux.(unseal).
+Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
 
 Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPred :=
   (* monPred_upclosed is not actually needed, since fupd is always
@@ -256,8 +256,8 @@ Definition monPred_fupd_def `{FUpd PROP} (E1 E2 : coPset) (P : monPred) : monPre
      terms in logical terms. *)
   monPred_upclosed (λ i, |={E1,E2}=> P i)%I.
 Definition monPred_fupd_aux `{FUpd PROP} : seal monPred_fupd_def. by eexists. Qed.
-Definition monPred_fupd `{FUpd PROP} : FUpd _ := unseal monPred_fupd_aux.
-Definition monPred_fupd_eq `{FUpd PROP} : @fupd _ monPred_fupd = _ := seal_eq _.
+Definition monPred_fupd `{FUpd PROP} : FUpd _ := monPred_fupd_aux.(unseal).
+Definition monPred_fupd_eq `{FUpd PROP} : @fupd _ monPred_fupd = _ := monPred_fupd_aux.(seal_eq).
 End Sbi.
 
 Module MonPred.

theories/program_logic/total_weakestpre.v

@@ -51,8 +51,8 @@ Definition twp_def `{irisG Λ Σ} (s : stuckness) (E : coPset)
     (e : expr Λ) (Φ : val Λ → iProp Σ) :
   iProp Σ := bi_least_fixpoint (twp_pre' s) (E,e,Φ).
 Definition twp_aux : seal (@twp_def). by eexists. Qed.
-Definition twp := unseal twp_aux.
-Definition twp_eq : @twp = @twp_def := seal_eq twp_aux.
+Definition twp := twp_aux.(unseal).
+Definition twp_eq : @twp = @twp_def := twp_aux.(seal_eq).
 
 Arguments twp {_ _ _} _ _ _%E _.
 Instance: Params (@twp) 6.

theories/program_logic/weakestpre.v

@@ -45,8 +45,8 @@ Qed.
 Definition wp_def `{irisG Λ Σ} (s : stuckness) :
   coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
 Definition wp_aux : seal (@wp_def). by eexists. Qed.
-Definition wp := unseal wp_aux.
-Definition wp_eq : @wp = @wp_def := seal_eq wp_aux.
+Definition wp := wp_aux.(unseal).
+Definition wp_eq : @wp = @wp_def := wp_aux.(seal_eq).
 
 Arguments wp {_ _ _} _ _ _%E _.
 Instance: Params (@wp) 6.

theories/proofmode/coq_tactics.v

@@ -29,8 +29,8 @@ Arguments of_envs : simpl never.
    proofmode's own tactics, such as [iIntros (?)]. *)
 Definition envs_entails_aux : seal (λ PROP (Δ : envs PROP) (Q : PROP), (of_envs Δ ⊢ Q)).
 Proof. by eexists. Qed.
-Definition envs_entails := unseal envs_entails_aux.
-Definition envs_entails_eq : envs_entails = _ := seal_eq envs_entails_aux.
+Definition envs_entails := envs_entails_aux.(unseal).
+Definition envs_entails_eq : envs_entails = _ := envs_entails_aux.(seal_eq).
 Arguments envs_entails {PROP} Δ Q%I : rename.
 Instance: Params (@envs_entails) 1.
 

[Robbert Krebbers]

What's the reason for this change? Does it actually improve performance or something?

[Ralf Jung]

@ppedrot suggested we use this to not (or less) rely on the compatibility layer.