diff options
| -rw-r--r-- | vernac/comInductive.ml | 6 | ||||
| -rw-r--r-- | vernac/comInductive.mli | 53 |
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 |