From 8b5f7383202f19446c3f291050d4d21934a0b0af Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 31 Mar 2020 13:27:39 +0200
Subject: [PATCH] Add missing `Proof.` to sealing proofs

This helps async proof checking (see
https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/406#note_46759).

Done with
```
gsed -i 's/seal \(.*\)\. by eexists. Qed./seal \1. Proof. by eexists. Qed./' \
  $(find theories/ -name '*.v')
```

And checked by inspecting the output of:
```
git grep '\bseal\b'|fgrep -v 'Proof. by eexists. Qed.'
```
---
 theories/algebra/big_op.v                 |  6 ++--
 theories/algebra/ofe.v                    |  2 +-
 theories/base_logic/lib/fancy_updates.v   |  2 +-
 theories/base_logic/lib/gen_heap.v        |  6 ++--
 theories/base_logic/lib/invariants.v      |  2 +-
 theories/base_logic/lib/own.v             |  2 +-
 theories/base_logic/lib/proph_map.v       |  2 +-
 theories/base_logic/upred.v               | 30 +++++++++---------
 theories/bi/big_op.v                      |  2 +-
 theories/bi/lib/atomic.v                  |  2 +-
 theories/bi/monpred.v                     | 38 +++++++++++------------
 theories/program_logic/total_weakestpre.v |  2 +-
 theories/program_logic/weakestpre.v       |  2 +-
 theories/si_logic/siprop.v                | 16 +++++-----
 14 files changed, 57 insertions(+), 57 deletions(-)

diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 4ea5f8f7b..ef7720273 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -37,7 +37,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
 
 Definition big_opM_def `{Monoid M o} `{Countable K} {A} (f : K → A → M)
   (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
-Definition big_opM_aux : seal (@big_opM_def). by eexists. Qed.
+Definition big_opM_aux : seal (@big_opM_def). Proof. by eexists. Qed.
 Definition big_opM := big_opM_aux.(unseal).
 Arguments big_opM {M} o {_ K _ _ A} _ _.
 Definition big_opM_eq : @big_opM = @big_opM_def := big_opM_aux.(seal_eq).
@@ -51,7 +51,7 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
 
 Definition big_opS_def `{Monoid M o} `{Countable A} (f : A → M)
   (X : gset A) : M := big_opL o (λ _, f) (elements X).
-Definition big_opS_aux : seal (@big_opS_def). by eexists. Qed.
+Definition big_opS_aux : seal (@big_opS_def). Proof. by eexists. Qed.
 Definition big_opS := big_opS_aux.(unseal).
 Arguments big_opS {M} o {_ A _ _} _ _.
 Definition big_opS_eq : @big_opS = @big_opS_def := big_opS_aux.(seal_eq).
@@ -62,7 +62,7 @@ Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
 
 Definition big_opMS_def `{Monoid M o} `{Countable A} (f : A → M)
   (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
-Definition big_opMS_aux : seal (@big_opMS_def). by eexists. Qed.
+Definition big_opMS_aux : seal (@big_opMS_def). Proof. by eexists. Qed.
 Definition big_opMS := big_opMS_aux.(unseal).
 Arguments big_opMS {M} o {_ A _ _} _ _.
 Definition big_opMS_eq : @big_opMS = @big_opMS_def := big_opMS_aux.(seal_eq).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index af1b04545..777559a15 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -303,7 +303,7 @@ 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_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_eq : @fixpoint = @fixpoint_def := fixpoint_aux.(seal_eq).
 
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 6317a7487..db4740283 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -9,7 +9,7 @@ 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_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).
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 2292f8d59..4a3065576 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -106,21 +106,21 @@ Section definitions.
 
   Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ :=
     own (gen_heap_name hG) (â—¯ {[ l := (q, to_agree (v : leibnizO V)) ]}).
-  Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
+  Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
 
   Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
     (∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
            own γm (namespace_map_token E))%I.
-  Definition meta_token_aux : seal (@meta_token_def). by eexists. Qed.
+  Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
   Definition meta_token := meta_token_aux.(unseal).
   Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
 
   Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
     (∃ γm, own (gen_meta_name hG) (◯ {[ l := to_agree γm ]}) ∗
            own γm (namespace_map_data N (to_agree (encode x))))%I.
-  Definition meta_aux : seal (@meta_def). by eexists. Qed.
+  Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
   Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
   Definition meta_eq : @meta = @meta_def := meta_aux.(seal_eq).
 End definitions.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 2d13f5937..790e5e51d 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -9,7 +9,7 @@ Import uPred.
 (** Semantic Invariants *)
 Definition inv_def `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   (□ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True))%I.
-Definition inv_aux : seal (@inv_def). by eexists. Qed.
+Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
 Definition inv {Σ i} := inv_aux.(unseal) Σ i.
 Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
 Instance: Params (@inv) 3 := {}.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index ae3d91ff5..82553775f 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -56,7 +56,7 @@ 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_aux : seal (@own_def). Proof. by eexists. Qed.
 Definition own {Σ A i} := own_aux.(unseal) Σ A i.
 Definition own_eq : @own = @own_def := own_aux.(seal_eq).
 Instance: Params (@own) 4 := {}.
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index b22092767..4b4c1c117 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -55,7 +55,7 @@ Section definitions.
   Definition proph_def (p : P) (vs : list V) : iProp Σ :=
     own (proph_map_name pG) (â—¯ {[p := Excl vs]}).
 
-  Definition proph_aux : seal (@proph_def). by eexists. Qed.
+  Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
   Definition proph := proph_aux.(unseal).
   Definition proph_eq : @proph = @proph_def := proph_aux.(seal_eq).
 End definitions.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index ee4335b04..2d7ce1524 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -192,7 +192,7 @@ Hint Resolve uPred_mono : uPred_def.
 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_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
 Definition uPred_pure {M} := uPred_pure_aux.(unseal) M.
 Definition uPred_pure_eq :
   @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
@@ -200,14 +200,14 @@ Definition uPred_pure_eq :
 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_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
 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_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
 Definition uPred_or {M} := uPred_or_aux.(unseal) M.
 Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
 
@@ -219,7 +219,7 @@ Next Obligation.
   rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
   eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc.
 Qed.
-Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. 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_eq :
   @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
@@ -227,7 +227,7 @@ Definition uPred_impl_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_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
 Definition uPred_forall {M A} := uPred_forall_aux.(unseal) M A.
 Definition uPred_forall_eq :
   @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
@@ -235,14 +235,14 @@ Definition uPred_forall_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_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
 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_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_eq:
   @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
@@ -254,7 +254,7 @@ Next Obligation.
   exists x1, (x2 â‹… z); split_and?; eauto using uPred_mono, cmra_includedN_l.
   eapply dist_le, Hn. by rewrite Hy Hx assoc.
 Qed.
-Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. 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_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
 
@@ -266,7 +266,7 @@ Next Obligation.
   eapply uPred_mono with n3 (x1 â‹… x3);
     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_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
 Definition uPred_wand {M} := uPred_wand_aux.(unseal) M.
 Definition uPred_wand_eq :
   @uPred_wand = @uPred_wand_def := uPred_wand_aux.(seal_eq).
@@ -277,7 +277,7 @@ Definition uPred_wand_eq :
 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). by eexists. Qed.
+Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. 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).
@@ -287,7 +287,7 @@ Program Definition uPred_persistently_def {M} (P : uPred M) : uPred M :=
 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_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
 Definition uPred_persistently {M} := uPred_persistently_aux.(unseal) M.
 Definition uPred_persistently_eq :
   @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
@@ -297,7 +297,7 @@ Program Definition uPred_later_def {M} (P : uPred M) : uPred M :=
 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_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
 Definition uPred_later {M} := uPred_later_aux.(unseal) M.
 Definition uPred_later_eq :
   @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
@@ -308,7 +308,7 @@ Next Obligation.
   intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn. eapply cmra_includedN_le=>//.
   exists (a' â‹… x2). by rewrite Hx(assoc op) Hx1.
 Qed.
-Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. 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_eq :
   @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
@@ -316,7 +316,7 @@ Definition uPred_ownM_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_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_eq :
   @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
@@ -331,7 +331,7 @@ Next Obligation.
   exists (x' â‹… x3); split; first by rewrite -assoc.
   eauto using uPred_mono, cmra_includedN_l.
 Qed.
-Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. 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_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 db2311abe..c274e6a75 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -54,7 +54,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
     (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
   (⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
    [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
-Definition big_sepM2_aux : seal (@big_sepM2_def). by eexists. Qed.
+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).
diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 318f4fbab..3e695fcff 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -87,7 +87,7 @@ Section definition.
 End definition.
 
 (** Seal it *)
-Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
+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).
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 3807d2f7f..cbf453aac 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -126,88 +126,88 @@ Program Definition monPred_upclosed (Φ : I → PROP) : monPred :=
 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_aux : seal (@monPred_embed_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_emp_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_pure_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_objectively_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_subjectively_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_and_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_or_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_impl_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_forall_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_exist_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_sep_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_wand_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_persistently_def). Proof. by eexists. Qed.
 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_aux : seal (@monPred_in_def). Proof. by eexists. Qed.
 Definition monPred_in := monPred_in_aux.(unseal).
 Definition monPred_in_eq : @monPred_in = _ := monPred_in_aux.(seal_eq).
 End Bi.
@@ -225,14 +225,14 @@ Implicit Types P Q : monPred.
 
 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_aux : seal (@monPred_internal_eq_def). Proof. by eexists. Qed.
 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_aux : seal monPred_later_def. Proof. by eexists. Qed.
 Definition monPred_later := monPred_later_aux.(unseal).
 Definition monPred_later_eq : monPred_later = _ := monPred_later_aux.(seal_eq).
 End Sbi.
@@ -768,7 +768,7 @@ 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. by eexists. 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).
@@ -865,7 +865,7 @@ 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. by eexists. 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).
@@ -902,7 +902,7 @@ 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. by eexists. Qed.
+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).
 
diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v
index 6b6b840be..955235d00 100644
--- a/theories/program_logic/total_weakestpre.v
+++ b/theories/program_logic/total_weakestpre.v
@@ -60,7 +60,7 @@ 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 Λ Σ _). by eexists. Qed.
+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).
 
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index ccbc2e5c2..4e90d18c6 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -46,7 +46,7 @@ Qed.
 
 Definition wp_def `{!irisG Λ Σ} (s : stuckness) :
   coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint (wp_pre s).
-Definition wp_aux `{!irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
+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).
 
diff --git a/theories/si_logic/siprop.v b/theories/si_logic/siprop.v
index 5619e0574..0edf0cb62 100644
--- a/theories/si_logic/siprop.v
+++ b/theories/si_logic/siprop.v
@@ -56,7 +56,7 @@ Hint Resolve siProp_closed : siProp_def.
 Program Definition siProp_pure_def (φ : Prop) : siProp :=
   {| siProp_holds n := φ |}.
 Solve Obligations with done.
-Definition siProp_pure_aux : seal (@siProp_pure_def). by eexists. Qed.
+Definition siProp_pure_aux : seal (@siProp_pure_def). Proof. by eexists. Qed.
 Definition siProp_pure := unseal siProp_pure_aux.
 Definition siProp_pure_eq :
   @siProp_pure = @siProp_pure_def := seal_eq siProp_pure_aux.
@@ -64,21 +64,21 @@ Definition siProp_pure_eq :
 Program Definition siProp_and_def (P Q : siProp) : siProp :=
   {| siProp_holds n := P n ∧ Q n |}.
 Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_and_aux : seal (@siProp_and_def). by eexists. Qed.
+Definition siProp_and_aux : seal (@siProp_and_def). Proof. by eexists. Qed.
 Definition siProp_and := unseal siProp_and_aux.
 Definition siProp_and_eq: @siProp_and = @siProp_and_def := seal_eq siProp_and_aux.
 
 Program Definition siProp_or_def (P Q : siProp) : siProp :=
   {| siProp_holds n := P n ∨ Q n |}.
 Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_or_aux : seal (@siProp_or_def). by eexists. Qed.
+Definition siProp_or_aux : seal (@siProp_or_def). Proof. by eexists. Qed.
 Definition siProp_or := unseal siProp_or_aux.
 Definition siProp_or_eq: @siProp_or = @siProp_or_def := seal_eq siProp_or_aux.
 
 Program Definition siProp_impl_def (P Q : siProp) : siProp :=
   {| siProp_holds n := ∀ n', n' ≤ n → P n' → Q n' |}.
 Next Obligation. intros P Q [|n1] [|n2]; auto with lia. Qed.
-Definition siProp_impl_aux : seal (@siProp_impl_def). by eexists. Qed.
+Definition siProp_impl_aux : seal (@siProp_impl_def). Proof. by eexists. Qed.
 Definition siProp_impl := unseal siProp_impl_aux.
 Definition siProp_impl_eq :
   @siProp_impl = @siProp_impl_def := seal_eq siProp_impl_aux.
@@ -86,7 +86,7 @@ Definition siProp_impl_eq :
 Program Definition siProp_forall_def {A} (Ψ : A → siProp) : siProp :=
   {| siProp_holds n := ∀ a, Ψ a n |}.
 Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_forall_aux : seal (@siProp_forall_def). by eexists. Qed.
+Definition siProp_forall_aux : seal (@siProp_forall_def). Proof. by eexists. Qed.
 Definition siProp_forall {A} := unseal siProp_forall_aux A.
 Definition siProp_forall_eq :
   @siProp_forall = @siProp_forall_def := seal_eq siProp_forall_aux.
@@ -94,14 +94,14 @@ Definition siProp_forall_eq :
 Program Definition siProp_exist_def {A} (Ψ : A → siProp) : siProp :=
   {| siProp_holds n := ∃ a, Ψ a n |}.
 Solve Obligations with naive_solver eauto 2 with siProp_def.
-Definition siProp_exist_aux : seal (@siProp_exist_def). by eexists. Qed.
+Definition siProp_exist_aux : seal (@siProp_exist_def). Proof. by eexists. Qed.
 Definition siProp_exist {A} := unseal siProp_exist_aux A.
 Definition siProp_exist_eq: @siProp_exist = @siProp_exist_def := seal_eq siProp_exist_aux.
 
 Program Definition siProp_internal_eq_def {A : ofeT} (a1 a2 : A) : siProp :=
   {| siProp_holds n := a1 ≡{n}≡ a2 |}.
 Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
-Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). by eexists. Qed.
+Definition siProp_internal_eq_aux : seal (@siProp_internal_eq_def). Proof. by eexists. Qed.
 Definition siProp_internal_eq {A} := unseal siProp_internal_eq_aux A.
 Definition siProp_internal_eq_eq:
   @siProp_internal_eq = @siProp_internal_eq_def := seal_eq siProp_internal_eq_aux.
@@ -109,7 +109,7 @@ Definition siProp_internal_eq_eq:
 Program Definition siProp_later_def (P : siProp) : siProp :=
   {| siProp_holds n := match n return _ with 0 => True | S n' => P n' end |}.
 Next Obligation. intros P [|n1] [|n2]; eauto using siProp_closed with lia. Qed.
-Definition siProp_later_aux : seal (@siProp_later_def). by eexists. Qed.
+Definition siProp_later_aux : seal (@siProp_later_def). Proof. by eexists. Qed.
 Definition siProp_later := unseal siProp_later_aux.
 Definition siProp_later_eq :
   @siProp_later = @siProp_later_def := seal_eq siProp_later_aux.
-- 
GitLab