diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index 949a2f027180a4a41da9da877892443395202d9a..145c9471ff250ea5bb961dc104d05d4486b0b340 100644
--- a/theories/typing/tests/init_prod.v
+++ b/theories/typing/tests/init_prod.v
@@ -4,7 +4,7 @@ From lrust.typing Require Import programs product product_split own uniq_bor
                     shr_bor int function lft_contexts uninit cont borrow.
 Set Default Proof Using "Type".
 
-Section rebor.
+Section init_prod.
   Context `{typeG Σ}.
 
   Definition init_prod : val :=
@@ -29,4 +29,4 @@ Section rebor.
     eapply type_delete; [solve_typing..|].
     eapply (type_jump [_]); solve_typing.
   Qed.
-End rebor.
+End init_prod.