From ac14add1ef27a3c650b825c8a567e0515d32d58d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 17 Jun 2019 05:10:36 +0200
Subject: [vernac] Cleanup on interface of Vernacentries

---
 ide/idetop.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/idetop.ml b/ide/idetop.ml
index c38b8fa820..c6a8fdaa55 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -429,6 +429,11 @@ let quit = ref false
 (** Disabled *)
 let print_ast id = Xml_datatype.PCData "ERROR"
 
+let idetop_make_cases iname =
+  let qualified_iname = Libnames.qualid_of_string iname in
+  let iref = Nametab.global_inductive qualified_iname in
+  ComInductive.make_cases iref
+
 (** Grouping all call handlers together + error handling *)
 let eval_call c =
   let interruptible f x =
@@ -449,7 +454,7 @@ let eval_call c =
     Interface.search = interruptible search;
     Interface.get_options = interruptible get_options;
     Interface.set_options = interruptible set_options;
-    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.mkcases = interruptible idetop_make_cases;
     Interface.quit = (fun () -> quit := true);
     Interface.init = interruptible init;
     Interface.about = interruptible about;
-- 
cgit v1.2.3