1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: type_errors.mli 10533 2008-02-08 16:54:47Z msozeau $ i*)
17
(* Type errors. \label{typeerrors} *)
19
(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
23
| NotEnoughAbstractionInFixBody
24
| RecursionNotOnInductiveType of constr
25
| RecursionOnIllegalTerm of int * constr * int list * int list
26
| NotEnoughArgumentsForFixCall of int
28
| CodomainNotInductiveType of constr
29
| NestedRecursiveOccurrences
30
| UnguardedRecursiveCall of constr
31
| RecCallInTypeOfAbstraction of constr
32
| RecCallInNonRecArgOfConstructor of constr
33
| RecCallInTypeOfDef of constr
34
| RecCallInCaseFun of constr
35
| RecCallInCaseArg of constr
36
| RecCallInCasePred of constr
37
| NotGuardedForm of constr
40
| NonInformativeToInformative
41
| StrongEliminationOnNonSmallType
46
| UnboundVar of variable
47
| NotAType of unsafe_judgment
48
| BadAssumption of unsafe_judgment
49
| ReferenceVariables of constr
50
| ElimArity of inductive * sorts_family list * constr * unsafe_judgment
51
* (sorts_family * sorts_family * arity_error) option
52
| CaseNotInductive of unsafe_judgment
53
| WrongCaseInfo of inductive * case_info
54
| NumberBranches of unsafe_judgment * int
55
| IllFormedBranch of constr * int * constr * constr
56
| Generalization of (name * types) * unsafe_judgment
57
| ActualType of unsafe_judgment * types
59
(int * constr * constr) * unsafe_judgment * unsafe_judgment array
60
| CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array
61
| IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array
63
int * name array * unsafe_judgment array * types array
65
exception TypeError of env * type_error
67
val error_unbound_rel : env -> int -> 'a
69
val error_unbound_var : env -> variable -> 'a
71
val error_not_type : env -> unsafe_judgment -> 'a
73
val error_assumption : env -> unsafe_judgment -> 'a
75
val error_reference_variables : env -> constr -> 'a
77
val error_elim_arity :
78
env -> inductive -> sorts_family list -> constr -> unsafe_judgment ->
79
(sorts_family * sorts_family * arity_error) option -> 'a
81
val error_case_not_inductive : env -> unsafe_judgment -> 'a
83
val error_number_branches : env -> unsafe_judgment -> int -> 'a
85
val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a
87
val error_generalization : env -> name * types -> unsafe_judgment -> 'a
89
val error_actual_type : env -> unsafe_judgment -> types -> 'a
91
val error_cant_apply_not_functional :
92
env -> unsafe_judgment -> unsafe_judgment array -> 'a
94
val error_cant_apply_bad_type :
95
env -> int * constr * constr ->
96
unsafe_judgment -> unsafe_judgment array -> 'a
98
val error_ill_formed_rec_body :
99
env -> guard_error -> name array -> int -> env -> unsafe_judgment array -> 'a
101
val error_ill_typed_rec_body :
102
env -> int -> name array -> unsafe_judgment array -> types array -> 'a