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.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

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

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9c3f97696f..e66bf7e1b7 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -10,6 +10,7 @@ open API
 open Pp
 open Util
 open Names
+open ModPath
 open Namegen
 open Nameops
 open Libnames
@@ -45,7 +46,7 @@ let pp_apply2 st par args =
 
 let pr_binding = function
   | [] -> mt ()
-  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") Id.print l
 
 let pp_tuple_light f = function
   | [] -> mt ()
@@ -274,8 +275,8 @@ let params_ren_add, params_ren_mem =
   seen at this level.
 *)
 
-type visible_layer = { mp : module_path;
-		       params : module_path list;
+type visible_layer = { mp : ModPath.t;
+		       params : ModPath.t list;
 		       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
-- 
cgit v1.2.3