From ef0721ab5721dbec9599cda6279ee03f5411ef29 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Mar 2017 13:35:17 +0100
Subject: [PATCH] force typed_val to be used only on values

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

diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 28a52c0e..f2b6d69e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -82,7 +82,7 @@ End typing.
 Notation typed_instruction_ty E L T e ty :=
   (typed_instruction E L T e (λ v : val, [v ◁ ty%list%T]%TC)).
 
-Notation typed_val e ty := (∀ E L, typed_instruction_ty E L [] e ty).
+Notation typed_val v ty := (∀ E L, typed_instruction_ty E L [] (of_val v) ty).
 
 Section typing_rules.
   Context `{typeG Σ}.
-- 
GitLab