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 +-
 kernel/term_typing.ml  | 4 ----
 kernel/term_typing.mli | 3 ---
 3 files changed, 1 insertion(+), 8 deletions(-)

(limited to 'kernel')

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
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f773f800c6..faa4411e92 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -371,7 +371,3 @@ let translate_local_def env _id centry =
   | Undef _ | Primitive _ -> assert false
   in
   c, decl.cook_relevance, typ
-
-(* Insertion of inductive types. *)
-
-let translate_mind env kn mie = Indtypes.check_inductive env kn mie
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index d34c28138e..1fa5eca2e3 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -35,9 +35,6 @@ val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     constant_body
 
-val translate_mind :
-  env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
 val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
-- 
cgit v1.2.3