From c44ef565b7e66026439c40b14bed30a18daef762 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 12 Mar 2019 09:38:12 +0100
Subject: Remove Term_typing.translate_mind indirection

---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index edb1d0a02e..673f025c75 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -842,7 +842,7 @@ let check_mind mie lab =
 let add_mind l mie senv =
   let () = check_mind mie l in
   let kn = MutInd.make2 senv.modpath l in
-  let mib = Term_typing.translate_mind senv.env kn mie in
+  let mib = Indtypes.check_inductive senv.env kn mie in
   let mib =
     match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
   in
-- 
cgit v1.2.3