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

---
 plugins/extraction/g_extraction.ml4 | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/extraction/g_extraction.ml4')

diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 6cba83ef9..76b435410 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -20,7 +20,6 @@ open Genarg
 open Stdarg
 open Pp
 open Names
-open Nameops
 open Table
 open Extract_env
 
@@ -35,7 +34,7 @@ END
 
 let pr_int_or_id _ _ _ = function
   | ArgInt i -> int i
-  | ArgId id -> pr_id id
+  | ArgId id -> Id.print id
 
 ARGUMENT EXTEND int_or_id
   PRINTED BY pr_int_or_id
-- 
cgit v1.2.3