diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 1cb2cc05e8f2a3b2c6abf658c91cde9e3577d6b4..3a6884ecbf9b341f6a372ddeae8daa3c2482f9af 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.