From c6673311085963801a23965d7c48ddc23ff662f7 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 1 May 2020 14:45:53 +0200
Subject: [PATCH] Nits

---
 theories/logrel/term_types.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 9445b8c..9e09a8c 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -28,7 +28,7 @@ Definition lty_forall `{heapG Σ} {k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∀ A, WP w #() {{ ltty_car (C A) }})%I.
 Definition lty_exist {Σ k} (C : lty Σ k → ltty Σ) : ltty Σ :=
   Ltty (λ w, ∃ A, ▷ ltty_car (C A) w)%I.
-Definition lty_texist {Σ} {TT : ktele Σ} (C : kt → ltty Σ) : ltty Σ :=
+Definition lty_texist {Σ} {kt : ktele Σ} (C : ltys kt → ltty Σ) : ltty Σ :=
   ktele_fold (@lty_exist Σ) (λ x, x) (ktele_bind C).
 
 Definition lty_ref_mut `{heapG Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
-- 
GitLab