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 7dcaf9b13..c13dd3a92 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -213,7 +213,7 @@ and val_of_constr env c =
let reraise = Errors.push reraise in
let () = print_string "can not compile \n" in
let () = Format.print_flush () in
- raise reraise
+ iraise reraise
in
eval_to_patch env (to_memory ccfv)