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 (3)

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.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.pretyping/Pretype_errors/index.html

Module Pretype_errorsSource

The type of errors raised by the pretyper
Sourcetype unification_error =
  1. | OccurCheck of Evar.t * EConstr.constr
  2. | NotClean of EConstr.existential * Environ.env * EConstr.constr
  3. | NotSameArgSize
  4. | NotSameHead
  5. | NoCanonicalStructure
  6. | ConversionFailed of Environ.env * EConstr.constr * EConstr.constr
  7. | IncompatibleInstances of Environ.env * EConstr.existential * EConstr.constr * EConstr.constr
  8. | MetaOccurInBody of Evar.t
  9. | InstanceNotSameType of Evar.t * Environ.env * EConstr.types * EConstr.types
  10. | InstanceNotFunctionalType of Evar.t * Environ.env * EConstr.constr * EConstr.types
  11. | UnifUnivInconsistency of UGraph.univ_inconsistency
  12. | CannotSolveConstraint of Evd.evar_constraint * unification_error
  13. | ProblemBeyondCapabilities
Sourcetype position = (Names.Id.t * Locus.hyp_location_flag) option
Sourcetype position_reporting = (position * int) * EConstr.constr
Sourcetype subterm_unification_error = bool * position_reporting * position_reporting
Sourcetype pretype_error =
  1. | CantFindCaseType of EConstr.constr
    (*

    Old Case

    *)
  2. | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
    (*

    Type inference unification

    *)
  3. | UnifOccurCheck of Evar.t * EConstr.constr
    (*

    Tactic Unification

    *)
  4. | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
  5. | CannotUnify of EConstr.constr * EConstr.constr * unification_error option
  6. | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
  7. | CannotUnifyBindingType of EConstr.constr * EConstr.constr
  8. | CannotGeneralize of EConstr.constr
  9. | NoOccurrenceFound of EConstr.constr * Names.Id.t option
  10. | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * pretype_error) option
  11. | WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types
  12. | AbstractionOverMeta of Names.Name.t * Names.Name.t
  13. | NonLinearUnification of Names.Name.t * EConstr.constr
    (*

    Pretyping

    *)
  14. | VarNotFound of Names.Id.t
  15. | EvarNotFound of Names.Id.t
  16. | UnexpectedType of EConstr.constr * EConstr.constr * unification_error
  17. | NotProduct of EConstr.constr
  18. | TypingError of type_error
  19. | CantApplyBadTypeExplained of (EConstr.constr, EConstr.types) Type_errors.pcant_apply_bad_type * unification_error
  20. | CannotUnifyOccurrences of subterm_unification_error
  21. | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t
    (*

    unresolvable evar, connex component

    *)
  22. | DisallowedSProp
Sourceexception PretypeError of Environ.env * Evd.evar_map * pretype_error
Sourceval precatchable_exception : exn -> bool
Sourceval raise_type_error : ?loc:Loc.t -> (Environ.env * Evd.evar_map * type_error) -> 'a

Raising errors

Sourceval error_actual_type_core : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b
Sourceval error_cant_apply_not_functional : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
Sourceval error_cant_apply_bad_type : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> ?error:unification_error -> (int * EConstr.constr * EConstr.constr) -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b
Sourceval error_case_not_inductive : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
Sourceval error_ill_formed_branch : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> Constr.pconstructor -> EConstr.constr -> EConstr.constr -> 'b
Sourceval error_number_branches : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> int -> 'b
Sourceval error_ill_typed_rec_body : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> int -> Names.Name.t EConstr.binder_annot array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b
Sourceval error_not_a_type : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
Sourceval error_assumption : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b
Sourceval error_cannot_coerce : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.constr) -> 'b
Implicit arguments synthesis errors
Sourceval error_occur_check : Environ.env -> Evd.evar_map -> Evar.t -> EConstr.constr -> 'b
Sourceval error_unsolvable_implicit : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Evar.t -> Evd.unsolvability_explanation option -> 'b
Sourceval error_cannot_unify : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> ?reason:unification_error -> (EConstr.constr * EConstr.constr) -> 'b
Sourceval error_cannot_unify_local : Environ.env -> Evd.evar_map -> (EConstr.constr * EConstr.constr * EConstr.constr) -> 'b
Sourceval error_cannot_find_well_typed_abstraction : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr list -> (Environ.env * pretype_error) option -> 'b
Sourceval error_wrong_abstraction_type : Environ.env -> Evd.evar_map -> Names.Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b
Sourceval error_abstraction_over_meta : Environ.env -> Evd.evar_map -> Names.Name.t -> Names.Name.t -> 'b
Sourceval error_non_linear_unification : Environ.env -> Evd.evar_map -> Names.Name.t -> EConstr.constr -> 'b
Ml Case errors
Sourceval error_cant_find_case_type : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'b
Pretyping errors
Sourceval error_unexpected_type : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> unification_error -> 'b
Sourceval error_not_product : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'b
Sourceval error_var_not_found : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t -> 'b
Sourceval error_evar_not_found : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Names.Id.t -> 'b
Sourceval error_disallowed_sprop : Environ.env -> Evd.evar_map -> 'a
Typeclass errors
Sourceval unsatisfiable_constraints : Environ.env -> Evd.evar_map -> Evar.t option -> Evar.Set.t -> 'a
Sourceval unsatisfiable_exception : exn -> bool