package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type inductive_error =
  1. | NonPos of Environ.env * Constr.constr * Constr.constr
  2. | NotEnoughArgs of Environ.env * Constr.constr * Constr.constr
  3. | NotConstructor of Environ.env * Names.Id.t * Constr.constr * Constr.constr * int * int
  4. | NonPar of Environ.env * Constr.constr * int * Constr.constr * Constr.constr
  5. | SameNamesTypes of Names.Id.t
  6. | SameNamesConstructors of Names.Id.t
  7. | SameNamesOverlap of Names.Id.t list
  8. | NotAnArity of Environ.env * Constr.constr
  9. | BadEntry
  10. | LargeNonPropInductiveNotInType
exception InductiveError of inductive_error
val enforce_indices_matter : unit -> unit
val is_indices_matter : unit -> bool