coq 8.7.1 · OCaml Package

type unification_error =

| OccurCheck of Term.existential_key * EConstr.constr
| NotClean of EConstr.existential * Environ.env * EConstr.constr
| NotSameArgSize
| NotSameHead
| NoCanonicalStructure
| ConversionFailed of Environ.env * EConstr.constr * EConstr.constr
| MetaOccurInBody of Term.existential_key
| InstanceNotSameType of Term.existential_key * 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 Term.existential_key * EConstr.constr
| UnsolvableImplicit of Term.existential_key * 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
| UnexpectedType of EConstr.constr * EConstr.constr
| NotProduct of EConstr.constr
| TypingError of type_error
| CannotUnifyOccurrences of subterm_unification_error
| 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_elim_arity : 
  ?loc:Loc.t ->
  Environ.env ->
  Evd.evar_map ->
  Term.pinductive ->
  Term.sorts_family list ->
  EConstr.constr ->
  EConstr.unsafe_judgment ->
  (Term.sorts_family * Term.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 ->
  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

package coq