diff options
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 66 |
1 files changed, 40 insertions, 26 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7587bd165f..cc104b3762 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Vernacexpr open Constrexpr @@ -42,37 +41,52 @@ val do_mutual_inductive val make_cases : Names.inductive -> string list list +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> DeclareInd.one_inductive_impls list + -> Names.MutInd.t + [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] + +val interp_mutual_inductive_constr + : sigma:Evd.evar_map + -> template:bool option + -> udecl:UState.universe_decl + -> 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) list + -> env_ar_params:Environ.env + (** Environment with the inductives and parameters in the rel_context *) + -> cumulative:bool + -> poly:bool + -> private_ind:bool + -> finite:Declarations.recursivity_kind + -> Entries.mutual_inductive_entry * UnivNames.universe_binders + (************************************************************************) (** Internal API, exported for Record *) (************************************************************************) -(** Registering a mutual inductive definition together with its - associated schemes *) - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - -val declare_mutual_inductive_with_eliminations : - ?primitive_expected:bool -> - mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> - MutInd.t - 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. *) -val template_polymorphism_candidate : - Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate env uctx params conclsort] is - [true] iff an inductive with params [params] and conclusion - [conclsort] would be definable as template polymorphic. It should - have at least one universe in its monomorphic universe context that - can be made parametric in its conclusion sort, if one is given. - If the [Template Check] flag is false we just check that the conclusion sort - is not small. *) - -val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t -(** [sign_level env sigma ctx] computes the universe level of the context [ctx] - as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) +val template_polymorphism_candidate + : template_check:bool + -> ctor_levels:Univ.LSet.t + -> Entries.universes_entry + -> Constr.rel_context + -> Sorts.t option + -> bool +(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params + conclsort] is [true] iff an inductive with params [params], + conclusion [conclsort] and universe levels appearing in the + constructor arguments [ctor_levels] would be definable as template + polymorphic. It should have at least one universe in its + monomorphic universe context that can be made parametric in its + conclusion sort, if one is given. If the [template_check] flag is + false we just check that the conclusion sort is not small. *) |