From 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 28 Jan 2013 21:05:35 +0000 Subject: Uniformization of the "anomaly" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/nativeconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/nativeconv.ml') 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 -- cgit v1.2.3