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/modutil.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 2b1e810604..6c38813e4b 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -8,6 +8,7 @@
 
 open API
 open Names
+open ModPath
 open Globnames
 open CErrors
 open Util
@@ -111,7 +112,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
     do_type (IndRef ip);
     if lang () == Ocaml then
       (match ind.ind_equiv with
-	 | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip));
+	 | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
-- 
cgit v1.2.3