package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.kernel/Modops/index.html

Module ModopsSource

Various operations on modules and module types

Functors

Sourceval is_functor : ('ty, 'a) Declarations.functorize -> bool
Sourceval destr_functor : ('ty, 'a) Declarations.functorize -> Names.MBId.t * 'ty * ('ty, 'a) Declarations.functorize
Sourceval destr_nofunctor : Names.ModPath.t -> ('ty, 'a) Declarations.functorize -> 'a
Sourceval check_modpath_equiv : Environ.env -> Names.ModPath.t -> Names.ModPath.t -> unit
Sourceval annotate_struct_body : Mod_declarations.structure_body -> Mod_declarations.module_signature -> Mod_declarations.module_signature
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.

add an abstract module parameter to the environment

Sourceval add_retroknowledge : Retroknowledge.action list -> Environ.env -> Environ.env
Strengthening
Sourceval strengthen_and_subst_module_body : Names.ModPath.t -> Mod_declarations.module_body -> Names.ModPath.t -> bool -> Mod_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
Sourcetype signature_mismatch_error =
  1. | InductiveFieldExpected of Declarations.mutual_inductive_body
  2. | DefinitionFieldExpected
  3. | ModuleFieldExpected
  4. | ModuleTypeFieldExpected
  5. | NotConvertibleInductiveField of Names.Id.t * (Environ.env * Constr.types * Constr.types) option
  6. | NotConvertibleConstructorField of Names.Id.t * (Environ.env * Constr.types * Constr.types) option
  7. | NotConvertibleBodyField of (Environ.env * Constr.constr * Constr.constr) option
  8. | NotConvertibleTypeField of Environ.env * Constr.types * Constr.types
  9. | CumulativeStatusExpected of bool
  10. | PolymorphicStatusExpected of bool
  11. | NotSameConstructorNamesField of Names.Id.t array * Names.Id.t array
  12. | NotSameInductiveNameInBlockField of Names.Id.t * Names.Id.t
  13. | FiniteInductiveFieldExpected of bool
  14. | InductiveNumbersFieldExpected of {
    1. got : int;
    2. expected : int;
    }
  15. | InductiveParamsNumberField of {
    1. got : int;
    2. expected : int;
    }
  16. | RecordFieldExpected of bool
  17. | RecordProjectionsExpected of {
    1. expected : Names.Name.t list;
    2. got : Names.Name.t list;
    }
  18. | NotEqualInductiveAliases of Names.MutInd.t * Names.MutInd.t
  19. | IncompatibleUniverses of {
    1. err : UGraph.univ_inconsistency;
    2. env : Environ.env;
    3. t1 : Constr.types;
    4. t2 : Constr.types;
    }
  20. | IncompatibleQualities of {
    1. err : QGraph.elimination_error;
    2. env : Environ.env;
    3. t1 : Constr.types;
    4. t2 : Constr.types;
    }
  21. | IncompatiblePolymorphism of Environ.env * Constr.types * Constr.types
  22. | IncompatibleUnivConstraints of {
    1. got : UVars.AbstractContext.t;
    2. expect : UVars.AbstractContext.t;
    }
  23. | IncompatibleVariance
  24. | NoRewriteRulesSubtyping
Sourcetype with_constraint_error =
  1. | WithSignatureMismatch of signature_mismatch_error
  2. | WithCannotConstrainPrimitive
  3. | WithCannotConstrainSymbol
Sourcetype subtyping_trace_elt =
  1. | Submodule of Names.Id.t
  2. | FunctorArgument of int
Sourcetype module_typing_error =
  1. | SignatureMismatch of subtyping_trace_elt list * Names.Id.t * signature_mismatch_error
  2. | LabelAlreadyDeclared of Names.Id.t
  3. | NotAFunctor
  4. | IsAFunctor of Names.ModPath.t
  5. | IncompatibleModuleTypes of Mod_declarations.module_type_body * Mod_declarations.module_type_body
  6. | NotEqualModulePaths of Names.ModPath.t * Names.ModPath.t
  7. | NoSuchLabel of Names.Id.t * Names.ModPath.t
  8. | NotAModuleLabel of Names.Id.t
  9. | NotAConstant of Names.Id.t
  10. | IncorrectWithConstraint of Names.Id.t * with_constraint_error
  11. | GenerativeModuleExpected of Names.Id.t
  12. | LabelMissing of Names.Id.t * string
  13. | IncludeRestrictedFunctor of Names.ModPath.t
Sourceexception ModuleTypingError of module_typing_error
Sourceval error_existing_label : Names.Id.t -> 'a
Sourceval error_signature_mismatch : subtyping_trace_elt list -> Names.Id.t -> signature_mismatch_error -> 'a
Sourceval error_no_such_label : Names.Id.t -> Names.ModPath.t -> 'a
Sourceval error_not_a_module_label : Names.Id.t -> 'a
Sourceval error_not_a_constant : Names.Id.t -> 'a
Sourceval error_incorrect_with_constraint : Names.Id.t -> with_constraint_error -> 'a
Sourceval error_generative_module_expected : Names.Id.t -> 'a
Sourceval error_no_such_label_sub : Names.Id.t -> string -> 'a
Sourceval error_include_restricted_functor : Names.ModPath.t -> 'a