package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
The type of errors raised by the pretyper
type 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. | UnifUnivInconsistency of Univ.univ_inconsistency
  11. | CannotSolveConstraint of Evd.evar_constraint * unification_error
  12. | ProblemBeyondCapabilities
type position = (Names.Id.t * Locus.hyp_location_flag) option
type position_reporting = (position * int) * EConstr.constr
type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option
type 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
  17. | NotProduct of EConstr.constr
  18. | TypingError of type_error
  19. | CannotUnifyOccurrences of subterm_unification_error
  20. | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option
    (*

    unresolvable evar, connex component

    *)
  21. | DisallowedSProp
exception PretypeError of Environ.env * Evd.evar_map * pretype_error
val precatchable_exception : exn -> bool
val error_actual_type : ?loc:Loc.t -> ?info:Exninfo.info -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> unification_error -> 'b

Raising errors

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