From b994e3195d296e9d12c058127ced381976c3a49e Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 31 May 2016 09:09:56 +0200
Subject: Checker: avoid using obsolete names from Names

---
 kernel/names.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/names.mli b/kernel/names.mli
index 1dfdd82903..56f0f8c60d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -766,7 +766,7 @@ val mind_of_kn : KerName.t -> mutual_inductive
 (** @deprecated Same as [MutInd.make1] *)
 
 val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make2] *)
+(** @deprecated Same as [MutInd.make] *)
 
 val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
 (** @deprecated Same as [MutInd.make3] *)
-- 
cgit v1.2.3