From b7505585b7817006336f55516de094893484f8fe Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 6 Jan 2017 00:15:48 +0100
Subject: [PATCH] Tweaking.

---
 theories/typing/product_split.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 2b0280bd..dfb8af8b 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -374,19 +374,19 @@ Section product_split.
     tyl ≠ [] →
     extract_tyl E L p (own n) tyl 0 T T' →
     tctx_extract_hasty E L p (own n (Π tyl)) T T'.
-  Proof. intro Htyl. apply tctx_extract_merge_ptr_prod, tctx_merge_own_prod, Htyl. Qed.
+  Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_own_prod. Qed.
 
   Lemma tctx_extract_merge_uniq_prod E L p κ tyl T T' :
     tyl ≠ [] →
     extract_tyl E L p (uniq_bor κ) tyl 0 T T' →
     tctx_extract_hasty E L p (&uniq{κ}Π tyl) T T'.
-  Proof. intro Htyl. apply tctx_extract_merge_ptr_prod, tctx_merge_uniq_prod, Htyl. Qed.
+  Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_uniq_prod. Qed.
 
   Lemma tctx_extract_merge_shr_prod E L p κ tyl T T' :
     tyl ≠ [] →
     extract_tyl E L p (shr_bor κ) tyl 0 T T' →
     tctx_extract_hasty E L p (&shr{κ}Π tyl) T T'.
-  Proof. intro Htyl. apply tctx_extract_merge_ptr_prod, tctx_merge_shr_prod, Htyl. Qed.
+  Proof. auto using tctx_extract_merge_ptr_prod, tctx_merge_shr_prod. Qed.
 End product_split.
 
 (* We make sure that this is applied after [tctx_extract_hasty_here] but before
-- 
GitLab