package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'constr pguard_error =
  1. | NotEnoughAbstractionInFixBody
  2. | RecursionNotOnInductiveType of 'constr
  3. | RecursionOnIllegalTerm of int * Environ.env * 'constr * int list * int list
  4. | NotEnoughArgumentsForFixCall of int
  5. | CodomainNotInductiveType of 'constr
  6. | NestedRecursiveOccurrences
  7. | UnguardedRecursiveCall of 'constr
  8. | RecCallInTypeOfAbstraction of 'constr
  9. | RecCallInNonRecArgOfConstructor of 'constr
  10. | RecCallInTypeOfDef of 'constr
  11. | RecCallInCaseFun of 'constr
  12. | RecCallInCaseArg of 'constr
  13. | RecCallInCasePred of 'constr
  14. | NotGuardedForm of 'constr
  15. | ReturnPredicateNotCoInductive of 'constr
type guard_error = Constr.constr pguard_error
type arity_error =
  1. | NonInformativeToInformative
  2. | StrongEliminationOnNonSmallType
  3. | WrongArity
type (!'constr, !'types) ptype_error =
  1. | UnboundRel of int
  2. | UnboundVar of Names.variable
  3. | NotAType of ('constr, 'types) Environ.punsafe_judgment
  4. | BadAssumption of ('constr, 'types) Environ.punsafe_judgment
  5. | ReferenceVariables of Names.Id.t * 'constr
  6. | ElimArity of Constr.pinductive * Sorts.family list * 'constr * ('constr, 'types) Environ.punsafe_judgment * (Sorts.family * Sorts.family * arity_error) option
  7. | CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
  8. | WrongCaseInfo of Constr.pinductive * Constr.case_info
  9. | NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
  10. | IllFormedBranch of 'constr * Constr.pconstructor * 'constr * 'constr
  11. | Generalization of Names.Name.t * 'types * ('constr, 'types) Environ.punsafe_judgment
  12. | ActualType of ('constr, 'types) Environ.punsafe_judgment * 'types
  13. | CantApplyBadType of int * 'constr * 'constr * ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
  14. | CantApplyNonFunctional of ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
  15. | IllFormedRecBody of 'constr pguard_error * Names.Name.t array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
  16. | IllTypedRecBody of int * Names.Name.t array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
  17. | UnsatisfiedConstraints of Univ.Constraint.t
  18. | UndeclaredUniverse of Univ.Level.t
exception TypeError of Environ.env * type_error
val error_unbound_rel : Environ.env -> int -> 'a
val error_unbound_var : Environ.env -> Names.variable -> 'a
val error_not_type : Environ.env -> Environ.unsafe_judgment -> 'a
val error_assumption : Environ.env -> Environ.unsafe_judgment -> 'a
val error_reference_variables : Environ.env -> Names.Id.t -> Constr.constr -> 'a
val error_case_not_inductive : Environ.env -> Environ.unsafe_judgment -> 'a
val error_number_branches : Environ.env -> Environ.unsafe_judgment -> int -> 'a
val error_ill_formed_branch : Environ.env -> Constr.constr -> Constr.pconstructor -> Constr.constr -> Constr.constr -> 'a
val error_generalization : Environ.env -> (Names.Name.t * Constr.types) -> Environ.unsafe_judgment -> 'a
val error_actual_type : Environ.env -> Environ.unsafe_judgment -> Constr.types -> 'a
val error_cant_apply_not_functional : Environ.env -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
val error_cant_apply_bad_type : Environ.env -> (int * Constr.constr * Constr.constr) -> Environ.unsafe_judgment -> Environ.unsafe_judgment array -> 'a
val error_ill_formed_rec_body : Environ.env -> guard_error -> Names.Name.t array -> int -> Environ.env -> Environ.unsafe_judgment array -> 'a
val error_ill_typed_rec_body : Environ.env -> int -> Names.Name.t array -> Environ.unsafe_judgment array -> Constr.types array -> 'a
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
val error_unsatisfied_constraints : Environ.env -> Univ.Constraint.t -> 'a
val error_undeclared_universe : Environ.env -> Univ.Level.t -> 'a