blob: 75962d11e2bdb75e08e07b30afcb2c698f481cb9 (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Util
open Names
open Term
open Sign
open Environ
open Glob_term
open Inductiveops
(** {6 The type of errors raised by the pretyper } *)
type pretype_error =
(** Old Case *)
| CantFindCaseType of constr
(** Unification *)
| OccurCheck of existential_key * constr
| NotClean of existential_key * constr * Evd.hole_kind
| UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
Evd.unsolvability_explanation option
| CannotUnify of constr * constr
| CannotUnifyLocal of constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * identifier option
| CannotFindWellTypedAbstraction of constr * constr list
| AbstractionOverMeta of name * name
| NonLinearUnification of name * constr
(** Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
| NotProduct of constr
| TypingError of Type_errors.type_error
exception PretypeError of env * Evd.evar_map * pretype_error
val precatchable_exception : exn -> bool
(** Presenting terms without solved evars *)
val nf_evar : Evd.evar_map -> constr -> constr
val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
val env_nf_evar : Evd.evar_map -> env -> env
val env_nf_betaiotaevar : Evd.evar_map -> env -> env
val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
val jv_nf_betaiotaevar :
Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
(** Raising errors *)
val error_actual_type_loc :
loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
val error_cant_apply_not_functional_loc :
loc -> env -> Evd.evar_map ->
unsafe_judgment -> unsafe_judgment list -> 'b
val error_cant_apply_bad_type_loc :
loc -> env -> Evd.evar_map -> int * constr * constr ->
unsafe_judgment -> unsafe_judgment list -> 'b
val error_case_not_inductive_loc :
loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
val error_ill_formed_branch_loc :
loc -> env -> Evd.evar_map ->
constr -> constructor -> constr -> constr -> 'b
val error_number_branches_loc :
loc -> env -> Evd.evar_map ->
unsafe_judgment -> int -> 'b
val error_ill_typed_rec_body_loc :
loc -> env -> Evd.evar_map ->
int -> name array -> unsafe_judgment array -> types array -> 'b
val error_not_a_type_loc :
loc -> env -> Evd.evar_map -> unsafe_judgment -> 'b
val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
(** {6 Implicit arguments synthesis errors } *)
val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
val error_not_clean :
env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
val error_unsolvable_implicit :
loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind ->
Evd.unsolvability_explanation option -> 'b
val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
constr -> constr list -> 'b
val error_abstraction_over_meta : env -> Evd.evar_map ->
metavariable -> metavariable -> 'b
val error_non_linear_unification : env -> Evd.evar_map ->
metavariable -> constr -> 'b
(** {6 Ml Case errors } *)
val error_cant_find_case_type_loc :
loc -> env -> Evd.evar_map -> constr -> 'b
(** {6 Pretyping errors } *)
val error_unexpected_type_loc :
loc -> env -> Evd.evar_map -> constr -> constr -> 'b
val error_not_product_loc :
loc -> env -> Evd.evar_map -> constr -> 'b
(** {6 Error in conversion from AST to glob_constr } *)
val error_var_not_found_loc : loc -> identifier -> 'b
|
