coq 8.11.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
| FixpointOnIrrelevantInductive

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 * 'constr * ('constr, 'types) Environ.punsafe_judgment * (Sorts.family * 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
| IncorrectPrimitive of (CPrimitives.op_or_type, '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 Context.binder_annot array * int * Environ.env * ('constr, 'types) Environ.punsafe_judgment array
| IllTypedRecBody of int * Names.Name.t Context.binder_annot array * ('constr, 'types) Environ.punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Univ.Constraint.t
| UndeclaredUniverse of Univ.Level.t
| DisallowedSProp
| BadRelevance

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

exception TypeError of Environ.env * type_error

type inductive_error =

| NonPos of Environ.env * Constr.constr * Constr.constr
| NotEnoughArgs of Environ.env * Constr.constr * Constr.constr
| NotConstructor of Environ.env * Names.Id.t * Constr.constr * Constr.constr * int * int
| NonPar of Environ.env * Constr.constr * int * Constr.constr * Constr.constr
| SameNamesTypes of Names.Id.t
| SameNamesConstructors of Names.Id.t
| SameNamesOverlap of Names.Id.t list
| NotAnArity of Environ.env * Constr.constr
| BadEntry
| LargeNonPropInductiveNotInType
| BadUnivs

exception InductiveError of inductive_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 ->
  Constr.constr ->
  Environ.unsafe_judgment ->
  (Sorts.family * 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_incorrect_primitive : 
  Environ.env ->
  (CPrimitives.op_or_type, Constr.types) Environ.punsafe_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 Context.binder_annot array ->
  int ->
  Environ.env ->
  Environ.unsafe_judgment array ->
  'a

val error_ill_typed_rec_body : 
  Environ.env ->
  int ->
  Names.Name.t Context.binder_annot 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

val error_disallowed_sprop : Environ.env -> 'a

val error_bad_relevance : Environ.env -> 'a

val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error

val map_ptype_error : 
  ('c -> 'd) ->
  ('c, 'c) ptype_error ->
  ('d, 'd) ptype_error

package coq