Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Constropen Environopen Evdopen EConstropen Type_errors
(** {6 The type of errors raised by the pretyper } *)
type unification_error = | OccurCheck of Evar.t * constr | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr | IncompatibleInstances of env * existential * constr * constr | MetaOccurInBody of Evar.t | InstanceNotSameType of Evar.t * env * types option * types | InstanceNotFunctionalType of Evar.t * env * constr * types | UnifUnivInconsistency of UGraph.univ_inconsistency | CannotSolveConstraint of evar_constraint * unification_error | ProblemBeyondCapabilities
type position = (Id.t * Locus.hyp_location_flag) option
type position_reporting = (position * int) * constr
type subterm_unification_error = bool * position_reporting * position_reporting
type type_error = (constr, types, ERelevance.t) ptype_error
val of_type_error : Type_errors.type_error -> type_error
type pretype_error = | CantFindCaseType of constr (** Old Case *)
| ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Type inference unification *)
| UnifOccurCheck of Evar.t * constr (** Tactic Unification *)
| UnsolvableImplicit of Evar.t * unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr | CannotGeneralize of constr | NoOccurrenceFound of constr * Id.t option | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t | NonLinearUnification of Name.t * constr (** Pretyping *) | VarNotFound of Id.t | EvarNotFound of Id.t | UnexpectedType of constr * constr * unification_error | NotProduct of constr | TypingError of type_error | CantApplyBadTypeExplained of (constr,types) pcant_apply_bad_type * unification_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t (** unresolvable evar, connex component *) | NotAllowedSProp | NotAllowedElimination of bool * ESorts.t * inductive puniverses | NotAllowedDependentElimination of bool * inductive
exception PretypeError of env * evar_map * pretype_error
val precatchable_exception : exn -> bool
(** Raising errors *)val raise_type_error : ?loc:Loc.t -> env * evar_map * type_error -> 'a
val error_actual_type : ?loc:Loc.t -> ?info:Exninfo.info -> env -> evar_map -> unsafe_judgment -> constr -> unification_error -> 'b
val error_actual_type_core : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> constr -> 'b
val error_cant_apply_not_functional : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> unsafe_judgment array -> 'b
val error_cant_apply_bad_type : ?loc:Loc.t -> env -> evar_map -> ?error:unification_error -> int * constr * constr -> unsafe_judgment -> unsafe_judgment array -> 'b
val error_case_not_inductive : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> 'b
val error_ill_formed_branch : ?loc:Loc.t -> env -> evar_map -> constr -> pconstructor -> constr -> constr -> 'b
val error_number_branches : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> int -> 'b
val error_ill_typed_rec_body : ?loc:Loc.t -> env -> evar_map -> int -> Name.t binder_annot array -> unsafe_judgment array -> types array -> 'b
val error_elim_arity : ?loc:Loc.t -> env -> evar_map -> inductive puniverses -> constr -> ESorts.t option -> 'b
val error_not_a_type : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> 'b
val error_assumption : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> 'b
val error_cannot_coerce : ?loc:Loc.t -> env -> evar_map -> constr * constr -> 'b
(** {6 Implicit arguments synthesis errors } *)
val error_occur_check : ?loc:Loc.t -> env -> evar_map -> Evar.t -> constr -> 'b
val error_unsolvable_implicit : ?loc:Loc.t -> env -> evar_map -> Evar.t -> unsolvability_explanation option -> 'b
val error_cannot_unify : ?loc:Loc.t -> env -> evar_map -> ?reason:unification_error -> constr * constr -> 'b
val error_cannot_unify_local : ?loc:Loc.t -> env -> evar_map -> constr * constr * constr -> 'b
val error_cannot_find_well_typed_abstraction : ?loc:Loc.t -> env -> evar_map -> constr -> constr list -> (env * pretype_error) option -> 'b
val error_wrong_abstraction_type : ?loc:Loc.t -> env -> evar_map -> Name.t -> constr -> types -> types -> 'b
val error_abstraction_over_meta : ?loc:Loc.t -> env -> evar_map -> Name.t -> Name.t -> 'b
val error_non_linear_unification : ?loc:Loc.t -> env -> evar_map -> Name.t -> constr -> 'b
(** {6 Ml Case errors } *)
val error_cant_find_case_type : ?loc:Loc.t -> env -> evar_map -> constr -> 'b
(** {6 Pretyping errors } *)
val error_unexpected_type : ?loc:Loc.t -> env -> evar_map -> constr -> constr -> unification_error -> 'b
val error_not_product : ?loc:Loc.t -> env -> evar_map -> constr -> 'b
val error_var_not_found : ?loc:Loc.t -> env -> evar_map -> Id.t -> 'b
val error_evar_not_found : ?loc:Loc.t -> env -> evar_map -> Id.t -> 'b
val error_not_allowed_sprop : ?loc:Loc.t -> env -> evar_map -> 'a
val error_not_allowed_elimination : ?loc:Loc.t -> env -> evar_map -> bool -> ESorts.t -> inductive puniverses -> 'a
val error_not_allowed_dependent_elimination : ?loc:Loc.t -> env -> evar_map -> bool -> inductive -> 'a
(** {6 Typeclass errors } *)
val unsatisfiable_constraints : env -> evar_map -> Evar.t option -> Evar.Set.t -> 'a
val unsatisfiable_exception : exn -> bool