From 5b109c098a46e5083ba0cf98b5fe72312331770e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 15 Jun 2017 19:42:22 +0200
Subject: fix dev/base_include (thanks Zimmi48)

---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index defea713d8..f9af0696b1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -233,7 +233,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Coqloop
 let go = loop
-- 
cgit v1.2.3