diff options
| author | Jan-Oliver Kaiser | 2019-08-09 17:01:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-01 15:49:23 +0100 |
| commit | 78d4fb3dade71e55288a316bb04d567409982433 (patch) | |
| tree | b55926e8004c0d192f098625f41562649f999a53 /vernac/comInductive.mli | |
| parent | d00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (diff) | |
Expose universe processing in comInductive.
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 067fb3d2ca..45e539b1e4 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -49,6 +49,25 @@ val declare_mutual_inductive_with_eliminations -> Names.MutInd.t [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] +val interp_mutual_inductive_constr : + env0:Environ.env -> + sigma:Evd.evar_map -> + template:bool option -> + udecl:UState.universe_decl -> + env_ar:Environ.env -> + env_params:Environ.env -> + ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> + indnames:Names.Id.t list -> + arities:EConstr.t list -> + arityconcl:(bool * EConstr.ESorts.t) option list -> + constructors:(Names.Id.t list * Constr.constr list * 'a list list) list -> + env_ar_params:Environ.env -> + cumulative:bool -> + poly:bool -> + private_ind:bool -> + finite:Declarations.recursivity_kind -> + Entries.mutual_inductive_entry * UnivNames.universe_binders + (************************************************************************) (** Internal API, exported for Record *) (************************************************************************) |