From 5e2e8693f4c63fb6c42ac81ea7c81c7c2e7e7fd8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Apr 2016 00:59:08 +0200
Subject: [PATCH] Remove forgotten Check.

---
 heap_lang/notation.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 1cb2cc05e..3a6884ecb 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -32,7 +32,6 @@ properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
 
-Check of_val'.
 Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
 Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
 
-- 
GitLab