From e9a6a3115d801140663c15341662918d9645681c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Jul 2019 19:07:36 +0200
Subject: [vernac] [inductive] Remove unused functions/exports.

The internal interpretation functions have been not used by funind
since some time.
---
 vernac/comInductive.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 65db4401d9..664010c917 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -80,9 +80,6 @@ type structured_one_inductive_expr = {
   ind_lc : (Id.t * constr_expr) list
 }
 
-type structured_inductive_expr =
-  local_binder_expr list * structured_one_inductive_expr list
-
 let minductive_message = function
   | []  -> user_err Pp.(str "No inductive definition.")
   | [x] -> (Id.print x ++ str " is defined")
@@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
-  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite
-
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
   List.equal local_binder_eq bl1 bl2
-- 
cgit v1.2.3