aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativevalues.ml')
-rw-r--r--kernel/nativevalues.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index fc4255aaf..2f317ca96 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -195,7 +195,8 @@ let mk_block tag args =
(* Two instances of dummy_value should not be pointer equal, otherwise
comparing them as terms would succeed *)
-let dummy_value : unit -> t = fun () _ -> anomaly "Evaluation failed"
+let dummy_value : unit -> t =
+ fun () _ -> anomaly ~label:"native" (Pp.str "Evaluation failed")
let cast_accu v = (Obj.magic v:accumulator)