package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
  2. | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
  3. | UnifOccurCheck of Evar.t * EConstr.constr
  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
  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
  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
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
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
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 -> 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
val unsatisfiable_constraints : Environ.env -> Evd.evar_map -> Evar.t option -> Evar.Set.t option -> 'a
val unsatisfiable_exception : exn -> bool