coq 8.8.2 · OCaml Package

coq

type !'constr pguard_error =

| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of 'constr
| RecursionOnIllegalTerm of int * Environ.env * 'constr * int list * int list
| NotEnoughArgumentsForFixCall of int
| CodomainNotInductiveType of 'constr
| NestedRecursiveOccurrences
| UnguardedRecursiveCall of 'constr
| RecCallInTypeOfAbstraction of 'constr
| RecCallInNonRecArgOfConstructor of 'constr
| RecCallInTypeOfDef of 'constr
| RecCallInCaseFun of 'constr
| RecCallInCaseArg of 'constr
| RecCallInCasePred of 'constr
| NotGuardedForm of 'constr
| ReturnPredicateNotCoInductive of 'constr

type guard_error = Constr.constr pguard_error

type arity_error =

| NonInformativeToInformative
| StrongEliminationOnNonSmallType
| WrongArity

type (!'constr, !'types) ptype_error =

| UnboundRel of int
| UnboundVar of Names.variable
| NotAType of ('constr, 'types) Environ.punsafe_judgment
| BadAssumption of ('constr, 'types) Environ.punsafe_judgment
| ReferenceVariables of Names.Id.t * 'constr
| ElimArity of Constr.pinductive * Sorts.family list * 'constr * ('constr, 'types) Environ.punsafe_judgment * (Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
| WrongCaseInfo of Constr.pinductive * Constr.case_info
| NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
| IllFormedBranch of 'constr * Constr.pconstructor * 'constr * 'constr
| Generalization of Names.Name.t * 'types * ('constr, 'types) Environ.punsafe_judgment
| ActualType of ('constr, 'types) Environ.punsafe_judgment * 'types
| CantApplyBadType of int * 'constr * 'constr * ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
| CantApplyNonFunctional of ('constr, 'types) Environ.punsafe_judgment * ('constr, 'types) Environ.punsafe_judgment array
| IllFormedRecBody of 'constr pguard_error * Names.Name.t array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
| IllTypedRecBody of int * Names.Name.t array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Univ.Constraint.t

type type_error = (Constr.constr, Constr.types) ptype_error

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_elim_arity : 
  Environ.env ->
  Constr.pinductive ->
  Sorts.family list ->
  Constr.constr ->
  Environ.unsafe_judgment ->
  (Sorts.family * Sorts.family * arity_error) option ->
  '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

package coq