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/mlutil.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 2655dfc897..6924dc9ffe 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -49,7 +49,7 @@ end
 
 (*s Utility functions over ML types without meta *)
 
-val type_mem_kn : mutual_inductive -> ml_type -> bool
+val type_mem_kn : MutInd.t -> ml_type -> bool
 
 val type_maxvar : ml_type -> int
 
-- 
cgit v1.2.3