aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-18 00:41:33 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-25 17:17:44 +0200
commitc9f9a159818c138af3b8d8a3a1023a66b88be207 (patch)
tree08f3a8ecb129753981150169e50cf5dd498623d0 /kernel
parent9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 (diff)
[feedback] Add optional ?loc parameter to loggers.
This is a first step to relay location info in an uniform way, as needed by warnings and other mechanisms. The location info remains unused for now, but coqtop printing could take advantage of it if so wished.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 431c914c0..a0ef5e570 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,7 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive tname ->
- let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in
+ let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning ?loc:None in
(Pp.(fn
(str "Cannot compile code for virtual machine as it uses inductive " ++
Id.print tname ++ str str_max_constructors));