Skip to content
Snippets Groups Projects
Commit ef0721ab authored by Ralf Jung's avatar Ralf Jung
Browse files

force typed_val to be used only on values

parent ba990862
No related branches found
No related tags found
No related merge requests found
......@@ -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 Σ}.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment