From 4c62c9f14bf08b59a018311a34dfa186e88c1b09 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 8 Jan 2019 18:41:23 +0100
Subject: [PATCH] update notations

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

diff --git a/theories/typing/types.v b/theories/typing/types.v
index 3426ea5..c466404 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -68,7 +68,7 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
 
 (** We model type-level lambdas and applications as thunks *)
 Notation "Λ: e" := (λ: <>, e)%E (at level 200).
-Notation "'TApp' e" := (e #())%E (at level 200).
+Notation "'TApp' e" := (App e%E #()%E) (at level 200).
 
 (* To unfold a recursive type, we need to take a step. We thus define the
 unfold operator to be the identity function. *)
-- 
GitLab