Skip to content

GitLab

Commit 5e2e8693 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove forgotten Check.

parent 7fc89711
Hide whitespace changes
Inline Side-by-side
heap_lang/notation.v
View file @ 5e2e8693
...@@ -32,7 +32,6 @@ properly. *) ...@@ -32,7 +32,6 @@ properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l"). Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope. 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 "' x" := (Var x) (at level 8, format "' x") : expr_scope.
Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope. Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment