diff options
author | 2016-06-18 00:41:33 +0200 | |
---|---|---|
committer | 2016-06-25 17:17:44 +0200 | |
commit | c9f9a159818c138af3b8d8a3a1023a66b88be207 (patch) | |
tree | 08f3a8ecb129753981150169e50cf5dd498623d0 /kernel | |
parent | 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 (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.ml | 2 |
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)); |