blob: 23a03290c83c7af499017cb4abe97fd62ec69c99 (
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
|
module SPretyping :
sig
module Cases :
sig
val compile_cases :
Util.loc ->
(Evarutil.type_constraint ->
Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment) *
Evd.evar_defs ref ->
Evarutil.type_constraint ->
Environ.env ->
Rawterm.rawconstr option *
(Rawterm.rawconstr *
(Names.name *
(Util.loc * Names.inductive * Names.name list) option))
list *
(Util.loc * Names.identifier list * Rawterm.cases_pattern list *
Rawterm.rawconstr)
list -> Environ.unsafe_judgment
end
val understand_tcc :
Evd.evar_map ->
Environ.env ->
?expected_type:Term.types -> Rawterm.rawconstr -> Evd.open_constr
val understand_ltac :
Evd.evar_map ->
Environ.env ->
Pretyping.var_map * Pretyping.unbound_ltac_var_map ->
Pretyping.typing_constraint ->
Rawterm.rawconstr -> Evd.evar_defs * Term.constr
val understand :
Evd.evar_map ->
Environ.env ->
?expected_type:Term.types -> Rawterm.rawconstr -> Term.constr
val understand_type :
Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
val understand_gen :
Pretyping.typing_constraint ->
Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
val understand_judgment :
Evd.evar_map ->
Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment
val understand_judgment_tcc :
Evd.evar_map ->
Environ.env ->
Rawterm.rawconstr -> Evd.evar_map * Environ.unsafe_judgment
val pretype :
Evarutil.type_constraint ->
Environ.env ->
Evd.evar_defs ref ->
Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
Rawterm.rawconstr -> Environ.unsafe_judgment
val pretype_type :
Evarutil.val_constraint ->
Environ.env ->
Evd.evar_defs ref ->
Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
Rawterm.rawconstr -> Environ.unsafe_type_judgment
val pretype_gen :
Evd.evar_defs ref ->
Environ.env ->
Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
Pretyping.typing_constraint -> Rawterm.rawconstr -> Term.constr
end
val interp_gen :
Pretyping.typing_constraint ->
Evd.evar_defs ref ->
Environ.env ->
?impls:Constrintern.full_implicits_env ->
?allow_soapp:bool ->
?ltacvars:Constrintern.ltac_sign ->
Topconstr.constr_expr -> Evd.evar_map * Term.constr
val interp_constr :
Evd.evar_defs ref ->
Environ.env -> Topconstr.constr_expr -> Evd.evar_map * Term.constr
val interp_type :
Evd.evar_defs ref ->
Environ.env ->
?impls:Constrintern.full_implicits_env ->
Topconstr.constr_expr -> Evd.evar_map * Term.constr
val interp_casted_constr :
Evd.evar_defs ref ->
Environ.env ->
?impls:Constrintern.full_implicits_env ->
Topconstr.constr_expr -> Term.types -> Evd.evar_map * Term.constr
val interp_open_constr :
Evd.evar_defs ref -> Environ.env -> Topconstr.constr_expr -> Term.constr
val interp_constr_judgment :
Evd.evar_defs ref ->
Environ.env ->
Topconstr.constr_expr -> Evd.evar_defs * Environ.unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
val collect_non_rec :
Environ.env ->
Names.identifier list ->
('a * Term.types) list ->
'b list ->
'c list ->
(Names.identifier * ('a * Term.types) * 'b) list *
(Names.identifier array * ('a * Term.types) array * 'b array * 'c array)
val recursive_message : Libnames.global_reference array -> Pp.std_ppcmds
val build_recursive :
(Topconstr.fixpoint_expr * Vernacexpr.decl_notation) list -> bool -> unit
|
