1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Names
open Constr
open Environ
(** Type errors. {% \label{typeerrors} %} *)
(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
notation i*)
type 'constr pguard_error =
(** Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of 'constr
| RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(** CoFixpoints *)
| 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 pguard_error
type arity_error =
| NonInformativeToInformative
| StrongEliminationOnNonSmallType
| WrongArity
type ('constr, 'types) ptype_error =
| UnboundRel of int
| UnboundVar of variable
| NotAType of ('constr, 'types) punsafe_judgment
| BadAssumption of ('constr, 'types) punsafe_judgment
| ReferenceVariables of Id.t * 'constr
| ElimArity of pinductive * Sorts.family list * 'constr * ('constr, 'types) punsafe_judgment
* (Sorts.family * Sorts.family * arity_error) option
| CaseNotInductive of ('constr, 'types) punsafe_judgment
| WrongCaseInfo of pinductive * case_info
| NumberBranches of ('constr, 'types) punsafe_judgment * int
| IllFormedBranch of 'constr * pconstructor * 'constr * 'constr
| Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment
| ActualType of ('constr, 'types) punsafe_judgment * 'types
| CantApplyBadType of
(int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array
| IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
| UnsatisfiedConstraints of Univ.Constraint.t
| UndeclaredUniverse of Univ.Level.t
type type_error = (constr, types) ptype_error
exception TypeError of env * type_error
(** The different kinds of errors that may result of a malformed inductive
definition. *)
type inductive_error =
| NonPos of env * constr * constr
| NotEnoughArgs of env * constr * constr
| NotConstructor of env * Id.t * constr * constr * int * int
| NonPar of env * constr * int * constr * constr
| SameNamesTypes of Id.t
| SameNamesConstructors of Id.t
| SameNamesOverlap of Id.t list
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
| BadUnivs
exception InductiveError of inductive_error
(** Raising functions *)
val error_unbound_rel : env -> int -> 'a
val error_unbound_var : env -> variable -> 'a
val error_not_type : env -> unsafe_judgment -> 'a
val error_assumption : env -> unsafe_judgment -> 'a
val error_reference_variables : env -> Id.t -> constr -> 'a
val error_elim_arity :
env -> pinductive -> Sorts.family list -> constr -> unsafe_judgment ->
(Sorts.family * Sorts.family * arity_error) option -> 'a
val error_case_not_inductive : env -> unsafe_judgment -> 'a
val error_number_branches : env -> unsafe_judgment -> int -> 'a
val error_ill_formed_branch : env -> constr -> pconstructor -> constr -> constr -> 'a
val error_generalization : env -> Name.t * types -> unsafe_judgment -> 'a
val error_actual_type : env -> unsafe_judgment -> types -> 'a
val error_cant_apply_not_functional :
env -> unsafe_judgment -> unsafe_judgment array -> 'a
val error_cant_apply_bad_type :
env -> int * constr * constr ->
unsafe_judgment -> unsafe_judgment array -> 'a
val error_ill_formed_rec_body :
env -> guard_error -> Name.t array -> int -> env -> unsafe_judgment array -> 'a
val error_ill_typed_rec_body :
env -> int -> Name.t array -> unsafe_judgment array -> types array -> 'a
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
val error_undeclared_universe : env -> Univ.Level.t -> 'a
|
