summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorChristopher Pulte2016-10-25 14:47:03 +0100
committerChristopher Pulte2016-10-25 14:47:03 +0100
commit2d7d954fe4f0bd3b1bac2afa3801f89ca23f25ed (patch)
treee9136ca62b6d876aadf979ebfe83fefa80714a21 /src
parentb8fa3ef036d9a7e4ae2c3fe1274ac08f5aeb40b6 (diff)
fix my decode_to_istate bug
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_inter_imp.lem2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index dad84a5c..cb5868ea 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -647,7 +647,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
(Interp_ast.Unknown, Nothing))
top_env Interp.eenv (Interp.emem "decode second top level") Interp.Top) Nothing) in
match (instr_decoded_error) with
- | Ivh_value instr -> IDE_instr instr_external instr
+ | Ivh_value _ -> IDE_instr instr_external instr
| Ivh_value_after_exn v ->
Assert_extra.failwith "supported_instructions called exit, so support will be needed for that now"
| Ivh_error err -> IDE_decode_error err