From 9705ff0d0673b9c2df8fa08c8aab01d2c40bc8f6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 4 Dec 2019 13:52:39 +0100
Subject: Avoid hardcoded paths in extraction

---
 plugins/extraction/common.mli | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction/common.mli')

diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index d13ac7926a..9dbc09dd06 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -70,10 +70,6 @@ val reset_renaming_tables : reset_kind -> unit
 
 val set_keywords : Id.Set.t -> unit
 
-(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
-
-val mk_ind : string -> string -> MutInd.t
-
 (** Special hack for constants of type Ascii.ascii : if an
     [Extract Inductive ascii => char] has been declared, then
     the constants are directly turned into chars *)
@@ -89,3 +85,6 @@ val pp_native_char : ml_ast -> Pp.t
 val is_native_string : ml_ast -> bool
 val get_native_string : ml_ast -> string
 val pp_native_string : ml_ast -> Pp.t
+
+(* Registered sig type *)
+val sig_type_ref : unit -> GlobRef.t
-- 
cgit v1.2.3