coq 8.7.2 · OCaml Package

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_type_of_module : 
  Declarations.module_body ->
  Declarations.module_type_body

val module_body_of_type : 
  Names.module_path ->
  Declarations.module_type_body ->
  Declarations.module_body

val check_modpath_equiv : 
  Environ.env ->
  Names.module_path ->
  Names.module_path ->
  unit

val implem_smartmap : 
  (Declarations.module_signature -> Declarations.module_signature) ->
  (Declarations.module_expression -> Declarations.module_expression) ->
  Declarations.module_implementation ->
  Declarations.module_implementation

val subst_signature : 
  Mod_subst.substitution ->
  Declarations.module_signature ->
  Declarations.module_signature

val subst_structure : 
  Mod_subst.substitution ->
  Declarations.structure_body ->
  Declarations.structure_body

val add_structure : 
  Names.module_path ->
  Declarations.structure_body ->
  Mod_subst.delta_resolver ->
  Environ.env ->
  Environ.env

val add_module : Declarations.module_body -> Environ.env -> Environ.env

val add_linked_module : 
  Declarations.module_body ->
  Pre_env.link_info ->
  Environ.env ->
  Environ.env

val add_module_type : 
  Names.module_path ->
  Declarations.module_type_body ->
  Environ.env ->
  Environ.env

val strengthen : 
  Declarations.module_type_body ->
  Names.module_path ->
  Declarations.module_type_body

val inline_delta_resolver : 
  Environ.env ->
  Entries.inline ->
  Names.module_path ->
  Names.MBId.t ->
  Declarations.module_type_body ->
  Mod_subst.delta_resolver ->
  Mod_subst.delta_resolver

val strengthen_and_subst_mb : 
  Declarations.module_body ->
  Names.module_path ->
  bool ->
  Declarations.module_body

val subst_modtype_and_resolver : 
  Declarations.module_type_body ->
  Names.module_path ->
  Declarations.module_type_body

val clean_bounded_mod_expr : 
  Declarations.module_signature ->
  Declarations.module_signature

val join_structure : 
  Future.UUIDSet.t ->
  Opaqueproof.opaquetab ->
  Declarations.structure_body ->
  unit

type signature_mismatch_error =

| InductiveFieldExpected of Declarations.mutual_inductive_body
| DefinitionFieldExpected
| ModuleFieldExpected
| ModuleTypeFieldExpected
| NotConvertibleInductiveField of Names.Id.t
| NotConvertibleConstructorField of Names.Id.t
| NotConvertibleBodyField
| NotConvertibleTypeField of Environ.env * Term.types * Term.types
| CumulativeStatusExpected of bool
| PolymorphicStatusExpected of bool
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
| FiniteInductiveFieldExpected of bool
| InductiveNumbersFieldExpected of int
| InductiveParamsNumberField of int
| RecordFieldExpected of bool
| RecordProjectionsExpected of Names.Name.t list
| NotEqualInductiveAliases
| NoTypeConstraintExpected
| IncompatibleInstances
| IncompatibleUniverses of Univ.univ_inconsistency
| IncompatiblePolymorphism of Environ.env * Term.types * Term.types
| IncompatibleConstraints of Univ.constraints

type module_typing_error =

| SignatureMismatch of Names.Label.t * Declarations.structure_field_body * signature_mismatch_error
| LabelAlreadyDeclared of Names.Label.t
| ApplicationToNotPath of Entries.module_struct_entry
| NotAFunctor
| IsAFunctor
| IncompatibleModuleTypes of Declarations.module_type_body * Declarations.module_type_body
| NotEqualModulePaths of Names.module_path * Names.module_path
| NoSuchLabel of Names.Label.t
| IncompatibleLabels of Names.Label.t * Names.Label.t
| NotAModule of string
| NotAModuleType of string
| NotAConstant of Names.Label.t
| IncorrectWithConstraint of Names.Label.t
| GenerativeModuleExpected of Names.Label.t
| LabelMissing of Names.Label.t * string
| IncludeRestrictedFunctor of Names.module_path

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_signature_mismatch : 
  Names.Label.t ->
  Declarations.structure_field_body ->
  signature_mismatch_error ->
  '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.module_path -> 'a

package coq