aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--exportclight/ExportClight.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 9937e5e7..e6d08d4f 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -288,7 +288,7 @@ let external_function p = function
signatur sg
(print_list coqstring) clob
| EF_profiling(id, kind) ->
- fprintf p "EF_profiling" (* should not happen *)
+ failwith "EF_profiling in ExportClight" (* should not happen *)
(* Expressions *)