blob: 9c0142866f9256aa17ffa1efd7474d50249aa144 (
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
132
133
|
open Term
open Libnames
open Coqlib
open Environ
open Pp
open Evd
open Decl_kinds
open Topconstr
open Rawterm
open Util
open Evarutil
open Names
open Sign
val ($) : ('a -> 'b) -> 'a -> 'b
val contrib_name : string
val subtac_dir : string list
val fix_sub_module : string
val fixsub_module : string list
val init_constant : string list -> string -> constr
val init_reference : string list -> string -> global_reference
val fixsub : constr lazy_t
val well_founded_ref : global_reference lazy_t
val acc_ref : global_reference lazy_t
val acc_inv_ref : global_reference lazy_t
val fix_sub_ref : global_reference lazy_t
val fix_measure_sub_ref : global_reference lazy_t
val lt_ref : global_reference lazy_t
val lt_wf_ref : global_reference lazy_t
val refl_ref : global_reference lazy_t
val sig_ref : reference
val proj1_sig_ref : reference
val proj2_sig_ref : reference
val build_sig : unit -> coq_sigma_data
val sig_ : coq_sigma_data lazy_t
val eq_ind : constr lazy_t
val eq_rec : constr lazy_t
val eq_rect : constr lazy_t
val eq_refl : constr lazy_t
val not_ref : constr lazy_t
val and_typ : constr lazy_t
val eqdep_ind : constr lazy_t
val eqdep_rec : constr lazy_t
val jmeq_ind : unit -> constr
val jmeq_rec : unit -> constr
val jmeq_refl : unit -> constr
val boolind : constr lazy_t
val sumboolind : constr lazy_t
val natind : constr lazy_t
val intind : constr lazy_t
val existSind : constr lazy_t
val existS : coq_sigma_data lazy_t
val prod : coq_sigma_data lazy_t
val well_founded : constr lazy_t
val fix : constr lazy_t
val acc : constr lazy_t
val acc_inv : constr lazy_t
val extconstr : constr -> constr_expr
val extsort : sorts -> constr_expr
val my_print_constr : env -> constr -> std_ppcmds
val my_print_constr_expr : constr_expr -> std_ppcmds
val my_print_evardefs : evar_defs -> std_ppcmds
val my_print_context : env -> std_ppcmds
val my_print_rel_context : env -> rel_context -> std_ppcmds
val my_print_named_context : env -> std_ppcmds
val my_print_env : env -> std_ppcmds
val my_print_rawconstr : env -> rawconstr -> std_ppcmds
val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
val debug : int -> std_ppcmds -> unit
val debug_msg : int -> std_ppcmds -> std_ppcmds
val trace : std_ppcmds -> unit
val wf_relations : (constr, constr lazy_t) Hashtbl.t
type binders = local_binder list
val app_opt : ('a -> 'a) option -> 'a -> 'a
val print_args : env -> constr array -> std_ppcmds
val make_existential : loc -> ?opaque:obligation_definition_status ->
env -> evar_defs ref -> types -> constr
val make_existential_expr : loc -> 'a -> 'b -> constr_expr
val string_of_hole_kind : hole_kind -> string
val evars_of_term : evar_map -> evar_map -> constr -> evar_map
val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map
val global_kind : logical_kind
val goal_kind : locality * goal_object_kind
val global_proof_kind : logical_kind
val goal_proof_kind : locality * goal_object_kind
val global_fix_kind : logical_kind
val goal_fix_kind : locality * goal_object_kind
val mkSubset : name -> constr -> constr -> constr
val mkProj1 : constr -> constr -> constr -> constr
val mkProj1 : constr -> constr -> constr -> constr
val mk_ex_pi1 : constr -> constr -> constr -> constr
val mk_ex_pi1 : constr -> constr -> constr -> constr
val mk_eq : types -> constr -> constr -> types
val mk_eq_refl : types -> constr -> constr
val mk_JMeq : types -> constr -> types -> constr -> types
val mk_JMeq_refl : types -> constr -> constr
val mk_conj : types list -> types
val mk_not : types -> types
val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
val destruct_ex : constr -> constr -> constr list
val id_of_name : name -> identifier
val definition_message : identifier -> std_ppcmds
val recursive_message : constant array -> std_ppcmds
val print_message : std_ppcmds -> unit
val solve_by_tac : evar_info -> Tacmach.tactic -> constr
val string_of_list : string -> ('a -> string) -> 'a list -> string
val string_of_intset : Intset.t -> string
val pr_evar_defs : evar_defs -> Pp.std_ppcmds
val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
|
