From 586d015eaa3d36a315bdbdf8b11593a9d00a9a9a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 15 Nov 2017 15:24:39 +0100
Subject: [dev] Remove deprecation warning from `base_include`

The warning created problems as OCaml restored the color printing tags
when printing it, so users doing `Drop` and then `go ()` got color
printing back after the warning.

We should guard the console on `Drop` better, but this requires some
(much needed) refactoring work in the toplevel.
---
 dev/base_include | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/base_include b/dev/base_include
index f2912e1127..1c98754fd4 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -231,7 +231,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 Id.Set.empty r));;
 
 let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
 
-- 
cgit v1.2.3