package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val is_functor : ('ty, 'a) Declarations.functorize -> bool
val destr_functor : ('ty, 'a) Declarations.functorize -> Names.MBId.t * 'ty * ('ty, 'a) Declarations.functorize
val destr_nofunctor : ('ty, 'a) Declarations.functorize -> 'a
val module_body_of_type : Names.ModPath.t -> Declarations.module_type_body -> Declarations.module_body
val check_modpath_equiv : Environ.env -> Names.ModPath.t -> Names.ModPath.t -> unit
val strengthen_and_subst_mb : Declarations.module_body -> Names.ModPath.t -> bool -> Declarations.module_body
type signature_mismatch_error =
  1. | InductiveFieldExpected of Declarations.mutual_inductive_body
  2. | DefinitionFieldExpected
  3. | ModuleFieldExpected
  4. | ModuleTypeFieldExpected
  5. | NotConvertibleInductiveField of Names.Id.t
  6. | NotConvertibleConstructorField of Names.Id.t
  7. | NotConvertibleBodyField
  8. | NotConvertibleTypeField of Environ.env * Constr.types * Constr.types
  9. | CumulativeStatusExpected of bool
  10. | PolymorphicStatusExpected of bool
  11. | NotSameConstructorNamesField
  12. | NotSameInductiveNameInBlockField
  13. | FiniteInductiveFieldExpected of bool
  14. | InductiveNumbersFieldExpected of int
  15. | InductiveParamsNumberField of int
  16. | RecordFieldExpected of bool
  17. | RecordProjectionsExpected of Names.Name.t list
  18. | NotEqualInductiveAliases
  19. | IncompatibleUniverses of Univ.univ_inconsistency
  20. | IncompatiblePolymorphism of Environ.env * Constr.types * Constr.types
  21. | IncompatibleConstraints of {
    1. got : Univ.AUContext.t;
    2. expect : Univ.AUContext.t;
    }
  22. | IncompatibleVariance
type module_typing_error =
  1. | SignatureMismatch of Names.Label.t * Declarations.structure_field_body * signature_mismatch_error
  2. | LabelAlreadyDeclared of Names.Label.t
  3. | ApplicationToNotPath of Entries.module_struct_entry
  4. | NotAFunctor
  5. | IsAFunctor
  6. | IncompatibleModuleTypes of Declarations.module_type_body * Declarations.module_type_body
  7. | NotEqualModulePaths of Names.ModPath.t * Names.ModPath.t
  8. | NoSuchLabel of Names.Label.t
  9. | IncompatibleLabels of Names.Label.t * Names.Label.t
  10. | NotAModule of string
  11. | NotAModuleType of string
  12. | NotAConstant of Names.Label.t
  13. | IncorrectWithConstraint of Names.Label.t
  14. | GenerativeModuleExpected of Names.Label.t
  15. | LabelMissing of Names.Label.t * string
  16. | IncludeRestrictedFunctor of Names.ModPath.t
exception ModuleTypingError of module_typing_error
val error_existing_label : Names.Label.t -> 'a
val error_incompatible_modtypes : Declarations.module_type_body -> Declarations.module_type_body -> 'a
val error_incompatible_labels : Names.Label.t -> Names.Label.t -> 'a
val error_no_such_label : Names.Label.t -> 'a
val error_not_a_module : string -> 'a
val error_not_a_constant : Names.Label.t -> 'a
val error_incorrect_with_constraint : Names.Label.t -> 'a
val error_generative_module_expected : Names.Label.t -> 'a
val error_no_such_label_sub : Names.Label.t -> string -> 'a
val error_include_restricted_functor : Names.ModPath.t -> 'a