Merge PR #10538: [vernac] [inductive] Remove unused functions/exports.

Reviewed-by: ppedrot

2 files changed, 11 insertions, 48 deletions

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
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 97f930c0a1..285be8cd51 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Entries
-open Libnames
 open Vernacexpr
 open Constrexpr
 
@@ -33,12 +32,20 @@ val do_mutual_inductive
   -> Declarations.recursivity_kind
   -> unit
 
+(** User-interface API *)
+
+(** Prepare a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables.
+    [Not_found] is raised if the given string isn't the qualid of
+    a known inductive type. *)
+
+val make_cases : Names.inductive -> string list list
+
 (************************************************************************)
-(** Internal API  *)
+(** Internal API, exported for Record                                   *)
 (************************************************************************)
 
-(** Exported for Record and Funind *)
-
 (** Registering a mutual inductive definition together with its
    associated schemes *)
 
@@ -55,41 +62,3 @@ val should_auto_template : Id.t -> bool -> bool
 (** [should_auto_template x b] is [true] when [b] is [true] and we
    automatically use template polymorphism. [x] is the name of the
    inductive under consideration. *)
-
-(** Exported for Funind *)
-
-(** Extracting the semantical components out of the raw syntax of mutual
-   inductive declarations *)
-
-type structured_one_inductive_expr = {
-  ind_name : Id.t;
-  ind_arity : constr_expr;
-  ind_lc : (Id.t * constr_expr) list
-}
-
-type structured_inductive_expr =
-  local_binder_expr list * structured_one_inductive_expr list
-
-val extract_mutual_inductive_declaration_components :
-  (one_inductive_expr * decl_notation list) list ->
-    structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
-
-(** Typing mutual inductive definitions *)
-val interp_mutual_inductive
-  :  template:bool option
-  -> universe_decl_expr option
-  -> structured_inductive_expr
-  -> decl_notation list
-  -> cumulative:bool
-  -> poly:bool
-  -> private_ind:bool
-  -> Declarations.recursivity_kind
-  -> mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
-
-(** Prepare a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables.
-    [Not_found] is raised if the given string isn't the qualid of
-    a known inductive type. *)
-
-val make_cases : Names.inductive -> string list list