From c9f9a159818c138af3b8d8a3a1023a66b88be207 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 18 Jun 2016 00:41:33 +0200
Subject: [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.
---
 kernel/cbytegen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 431c914c08..a0ef5e570e 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));
-- 
cgit v1.2.3