Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Environopen Entriesopen Declarations
module NotPrimRecordReason : sig
type t = | MustNotBeSquashed | MustHaveRelevantProj | MustHaveProj | MustNotHaveAnonProj
end
type inductive_arity = { user_arity : Constr.types; sort : Sorts.t }
(** Type checking for some inductive entry. Returns: - environment with inductives + parameters in rel context - abstracted universes - checked variance info (variance for section universes is at the beginning of the array) - record entry (checked to be OK) - if primitive record was requested, either: (1) if it's not ok, then why, or (2) whether it has eta - parameters - for each inductive, (arity * constructors) (with params) * (indices * splayed constructor types) (both without params) * top allowed elimination *)val typecheck_inductive : env -> sec_univs:UVars.Instance.t option -> mutual_inductive_entry -> env * universes * template_universes option * UVars.Variance.t array option * Names.Id.t array option option * (Declarations.has_eta, NotPrimRecordReason.t) result option * Constr.rel_context * ((inductive_arity * Constr.types array) * (Constr.rel_context * (Constr.rel_context * Constr.types) array) * squash_info option * bool (** true if the inductive relies on indices not mattering *)) array