Minor tweaks

theories/prophecy/prophecy.v

@@ -230,7 +230,7 @@ Notation "⟨ π , φ ⟩" := (proph_obs (λ π, φ%type%stdpp))
 
 (** * Iris Lemmas *)
 
-Section lemmas.
+Section proph.
 Context `{!invG Σ, !prophG Σ}.
 
 (** Instances *)
@@ -419,7 +419,7 @@ Proof.
   iMod (proph_obs_sat with "PROPH Obs") as %[? Ex]; [done|]. by apply Neg in Ex.
 Qed.
 
-End lemmas.
+End proph.
 
 Global Opaque proph_ctx proph_tok proph_obs.
 
@@ -430,7 +430,7 @@ Definition proph_eqz `{!invG Σ, !prophG Σ} {A} (uπ vπ: proph A) : iProp Σ :
 
 Notation "uπ :== vπ" := (proph_eqz uπ vπ) (at level 70, format "uπ  :==  vπ") : bi_scope.
 
-Section lemmas.
+Section proph_eqz.
 Context `{!invG Σ, !prophG Σ}.
 
 (** ** Constructing Prophecy Equalizers *)
@@ -499,4 +499,4 @@ Proof.
   iIntros "Eqz". rewrite !vapply_insert_backmid.
   iApply (proph_eqz_constr3 with "[] Eqz []"); iApply proph_eqz_refl.
 Qed.
-End lemmas.
+End proph_eqz.

theories/typing/array_idx.v

@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 
 Implicit Type 𝔄: syn_type.
 
-Section lemmas.
+Section array_idx.
   Context `{!typeG Σ}.
 
   (** * Owning Pointers *)
@@ -267,7 +267,7 @@ Section lemmas.
     iApply type_let; [by apply type_idx_uniq_array_instr|solve_typing| |done].
     move: Ex=> [Htrx _]?. apply Htrx. by case=> [?[??]].
   Qed.
-End lemmas.
+End array_idx.
 
 Global Hint Resolve tctx_extract_split_own_array
   tctx_extract_idx_shr_array tctx_extract_split_uniq_array | 5 : lrust_typing.

theories/typing/fixpoint.v

@@ -133,7 +133,7 @@ End fix_defs.
 Import fix_defs.
 Global Notation fix_ty := fix_ty.
 
-Section lemmas.
+Section fix_ty.
   Context `{!typeG Σ}.
 
   Lemma fix_unfold_fold {𝔄} (T: type 𝔄 → type 𝔄) {HT: TypeContractive T} E L :
@@ -244,9 +244,9 @@ Section lemmas.
     - move=> *. etrans; [apply conv_compl|].
       etrans; [|symmetry; apply conv_compl]. by apply Hne.
   Qed.
-End lemmas.
+End fix_ty.
 
-Section lemmas.
+Section fix_ty.
   Context `{!typeG Σ} {𝔄} (T: type 𝔄 → type 𝔄) {HT: TypeContractive T}.
 
   Global Instance fix_copy :
@@ -302,9 +302,9 @@ Section lemmas.
       apply limit_preserving_entails; [done|]=> ??? Eq;
       do 3 f_equiv; [apply Eq|]; do 5 f_equiv); [|do 2 f_equiv]; apply Eq.
   Qed.
-End lemmas.
+End fix_ty.
 
-Section subtyping.
+Section fix_subtyping.
   Context `{!typeG Σ}.
 
   Local Lemma wand_forall P (Φ: nat → iProp Σ) : (∀n, P -∗ Φ n) ⊢ (P -∗ ∀n, Φ n).
@@ -390,7 +390,7 @@ Section subtyping.
   Proof.
     move=> ?. eapply (eqtype_trans _ _ _ id id); [|done]. apply fix_unfold_fold.
   Qed.
-End subtyping.
+End fix_subtyping.
 
 Global Hint Resolve fix_subtype_l fix_subtype_r fix_eqtype_l fix_eqtype_r | 100
   : lrust_typing.