aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/nativeconv.ml')
-rw-r--r--kernel/nativeconv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 4ba305660..1c931ab85 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -148,6 +148,6 @@ let native_conv pb env t1 t2 =
(* TODO change 0 when we can have deBruijn *)
conv_val pb 0 !rt1 !rt2 empty_constraint
end
- | _ -> anomaly "Compilation failure"
+ | _ -> anomaly (Pp.str "Compilation failure")
let _ = set_nat_conv native_conv