From d63de7cb1be59bc7df492e652ac0b4bb88feb6a6 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 11 Jan 2017 00:51:57 +0100
Subject: [PATCH] Alpha renaming.

---
 theories/typing/tests/init_prod.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index 949a2f02..145c9471 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.
-- 
GitLab