diff options
| author | Maxime Dénès | 2018-02-24 09:33:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-24 09:33:03 +0100 |
| commit | bd41af496fd09d6ecd965190cad2873f1cd6b029 (patch) | |
| tree | 029c44d509cdaba200db07dfed61adb55b237f9e /kernel/csymtable.ml | |
| parent | c4aeaa7aedb04bf156a4946b05bad8f66d5eec69 (diff) | |
| parent | 557c5a2938f16c0601f5a0323c66b78d2da01ee9 (diff) | |
Merge PR #6784: New IR in VM: Clambda
Diffstat (limited to 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 55430a9d81..236d83576d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -164,7 +164,7 @@ and eval_to_patch env (buff,pl,fv) = eval_tcode tc vm_env and val_of_constr env c = - match compile true env c with + match compile ~fail_on_error:true env c with | Some v -> eval_to_patch env (to_memory v) | None -> assert false |