package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
Various operations on modules and module types

Functors

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 : Names.ModPath.t -> ('ty, 'a) Declarations.functorize -> 'a

Conversions between module_body and module_type_body

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
Substitutions
Adding to an environment

adds a module and its components, but not the constraints

same as add_module, but for a module whose native code has been linked by the native compiler. The linking information is updated.

same, for a module type

Strengthening
val strengthen_and_subst_module_body : Declarations.module_body -> Names.ModPath.t -> bool -> Declarations.module_body
Building map of constants to inline
Cleaning a module expression from bounded parts

For instance: functor(X:T)->struct module M:=X end) becomes: functor(X:T)->struct module M:=<content of T> end)

Errors
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 UGraph.univ_inconsistency
  20. | IncompatiblePolymorphism of Environ.env * Constr.types * Constr.types
  21. | IncompatibleConstraints of {
    1. got : Univ.AbstractContext.t;
    2. expect : Univ.AbstractContext.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. | NotAFunctor
  4. | IsAFunctor of Names.ModPath.t
  5. | IncompatibleModuleTypes of Declarations.module_type_body * Declarations.module_type_body
  6. | NotEqualModulePaths of Names.ModPath.t * Names.ModPath.t
  7. | NoSuchLabel of Names.Label.t * Names.ModPath.t
  8. | NotAModuleLabel of Names.Label.t
  9. | NotAConstant of Names.Label.t
  10. | IncorrectWithConstraint of Names.Label.t
  11. | GenerativeModuleExpected of Names.Label.t
  12. | LabelMissing of Names.Label.t * string
  13. | 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_no_such_label : Names.Label.t -> Names.ModPath.t -> 'a
val error_not_a_module_label : Names.Label.t -> '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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct