coq 8.11.1 · OCaml Package

type unification_error =

| OccurCheck of Evar.t * EConstr.constr
| NotClean of EConstr.existential * Environ.env * EConstr.constr
| NotSameArgSize
| NotSameHead
| NoCanonicalStructure
| ConversionFailed of Environ.env * EConstr.constr * EConstr.constr
| MetaOccurInBody of Evar.t
| InstanceNotSameType of Evar.t * Environ.env * EConstr.types * EConstr.types
| UnifUnivInconsistency of Univ.univ_inconsistency
| CannotSolveConstraint of Evd.evar_constraint * unification_error
| 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 type_error = (EConstr.constr, EConstr.types) Type_errors.ptype_error

type pretype_error =

| CantFindCaseType of EConstr.constr
| ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error
| UnifOccurCheck of Evar.t * EConstr.constr
| UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option
| CannotUnify of EConstr.constr * EConstr.constr * unification_error option
| CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr
| CannotUnifyBindingType of EConstr.constr * EConstr.constr
| CannotGeneralize of EConstr.constr
| NoOccurrenceFound of EConstr.constr * Names.Id.t option
| CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (Environ.env * type_error) option
| WrongAbstractionType of Names.Name.t * EConstr.constr * EConstr.types * EConstr.types
| AbstractionOverMeta of Names.Name.t * Names.Name.t
| NonLinearUnification of Names.Name.t * EConstr.constr
| VarNotFound of Names.Id.t
| EvarNotFound of Names.Id.t
| UnexpectedType of EConstr.constr * EConstr.constr
| NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
| UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option
| DisallowedSProp

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 ->
  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_elim_arity : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  Constr.pinductive ->
  EConstr.constr ->
  EConstr.unsafe_judgment ->
  (Sorts.family * Sorts.family * Sorts.family * Type_errors.arity_error) option ->
  '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 * 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 ->
  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

package coq