aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 55430a9d8..236d83576 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