From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/extraction/common.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

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

diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 4c9b1e1a5a..004019e168 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -50,20 +50,20 @@ type phase = Pre | Impl | Intf
 val set_phase : phase -> unit
 val get_phase : unit -> phase
 
-val opened_libraries : unit -> module_path list
+val opened_libraries : unit -> ModPath.t list
 
 type kind = Term | Type | Cons | Mod
 
 val pp_global : kind -> global_reference -> string
-val pp_module : module_path -> string
+val pp_module : ModPath.t -> string
 
-val top_visible_mp : unit -> module_path
+val top_visible_mp : unit -> ModPath.t
 (* In [push_visible], the [module_path list] corresponds to
    module parameters, the innermost one coming first in the list *)
-val push_visible : module_path -> module_path list -> unit
+val push_visible : ModPath.t -> ModPath.t list -> unit
 val pop_visible : unit -> unit
 
-val get_duplicate : module_path -> Label.t -> string option
+val get_duplicate : ModPath.t -> Label.t -> string option
 
 type reset_kind = AllButExternal | Everything
 
@@ -73,7 +73,7 @@ val set_keywords : Id.Set.t -> unit
 
 (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
 
-val mk_ind : string -> string -> mutual_inductive
+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
-- 
cgit v1.2.3