From cdceb6ac279196b04d3276cccdbbfce88bec2e4c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 11 Jun 2017 11:27:01 +0200
Subject: Fixing base_include after loc is an option (30d3515).

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

(limited to 'dev')

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