package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type unification_error =
  1. | OccurCheck of Term.existential_key * 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. | MetaOccurInBody of Term.existential_key
  8. | InstanceNotSameType of Term.existential_key * Environ.env * EConstr.types * EConstr.types
  9. | UnifUnivInconsistency of Univ.univ_inconsistency
  10. | CannotSolveConstraint of Evd.evar_constraint * unification_error
  11. | 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
  2. | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
  3. | UnifOccurCheck of Term.existential_key * EConstr.constr
  4. | UnsolvableImplicit of Term.existential_key * 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 * type_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
  14. | VarNotFound of Names.Id.t
  15. | UnexpectedType of EConstr.constr * EConstr.constr
  16. | NotProduct of EConstr.constr
  17. | TypingError of type_error
  18. | CannotUnifyOccurrences of subterm_unification_error
  19. | UnsatisfiableConstraints of (Term.existential_key * Evar_kinds.t) option * Evar.Set.t option
exception PretypeError of Environ.env * Evd.evar_map * pretype_error
val precatchable_exception : exn -> bool
val error_actual_type : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> unification_error -> 'b
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 -> Term.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 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
val error_occur_check : Environ.env -> Evd.evar_map -> Term.existential_key -> EConstr.constr -> 'b
val error_unsolvable_implicit : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Term.existential_key -> 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 * type_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 -> Term.metavariable -> Term.metavariable -> 'b
val error_non_linear_unification : Environ.env -> Evd.evar_map -> Term.metavariable -> EConstr.constr -> 'b
val error_cant_find_case_type : ?loc:Loc.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'b
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 -> Names.Id.t -> 'b
val unsatisfiable_constraints : Environ.env -> Evd.evar_map -> Evd.evar option -> Evar.Set.t option -> 'a
val unsatisfiable_exception : exn -> bool
OCaml

Innovation. Community. Security.