coq 8.7.1 · 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 = Term.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.identifier * 'constr
| ElimArity of Term.pinductive * Term.sorts_family list * 'constr * ('constr, 'types) Environ.punsafe_judgment * (Term.sorts_family * Term.sorts_family * arity_error) option
| CaseNotInductive of ('constr, 'types) Environ.punsafe_judgment
| WrongCaseInfo of Term.pinductive * Term.case_info
| NumberBranches of ('constr, 'types) Environ.punsafe_judgment * int
| IllFormedBranch of 'constr * Term.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.constraints

type type_error = (Term.constr, Term.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.identifier ->
  Term.constr ->
  'a

val error_elim_arity : 
  Environ.env ->
  Term.pinductive ->
  Term.sorts_family list ->
  Term.constr ->
  Environ.unsafe_judgment ->
  (Term.sorts_family * Term.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 ->
  Term.constr ->
  Term.pconstructor ->
  Term.constr ->
  Term.constr ->
  'a

val error_generalization : 
  Environ.env ->
  (Names.Name.t * Term.types) ->
  Environ.unsafe_judgment ->
  'a

val error_actual_type : 
  Environ.env ->
  Environ.unsafe_judgment ->
  Term.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 * Term.constr * Term.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 ->
  Term.types array ->
  'a

val error_elim_explain : Term.sorts_family -> Term.sorts_family -> arity_error

val error_unsatisfied_constraints : Environ.env -> Univ.constraints -> 'a

package coq