blob: 16beaaa3c736bbfb8aeca1c5a5d07e06da3ab6d1 (
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 Names
(*
The mk_?_id function build different name w.r.t. a function
Each of their use is justified in the code
*)
val mk_rel_id : Id.t -> Id.t
val mk_correct_id : Id.t -> Id.t
val mk_complete_id : Id.t -> Id.t
val mk_equation_id : Id.t -> Id.t
val msgnl : Pp.t -> unit
val fresh_id : Id.t list -> string -> Id.t
val fresh_name : Id.t list -> string -> Name.t
val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
val array_get_start : 'a array -> 'a array
val locate_ind : Libnames.qualid -> inductive
val locate_constant : Libnames.qualid -> Constant.t
val locate_with_msg :
Pp.t -> (Libnames.qualid -> 'a) ->
Libnames.qualid -> 'a
val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
val list_union_eq :
('a -> 'a -> bool) -> 'a list -> 'a list -> 'a list
val list_add_set_eq :
('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
val chop_rlambda_n : int -> Glob_term.glob_constr ->
(Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr
val chop_rprod_n : int -> Glob_term.glob_constr ->
(Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
val eq : EConstr.constr Lazy.t
val refl_equal : EConstr.constr Lazy.t
val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
val make_eq : unit -> EConstr.constr
val save
: Id.t
-> Evd.side_effects Proof_global.proof_entry
-> ?hook:DeclareDef.Hook.t
-> UState.t
-> DeclareDef.locality
-> Decls.logical_kind
-> unit
(* [with_full_print f a] applies [f] to [a] in full printing environment.
This function preserves the print settings
*)
val with_full_print : ('a -> 'b) -> 'a -> 'b
(*****************)
type function_info =
{
function_constant : Constant.t;
graph_ind : inductive;
equation_lemma : Constant.t option;
correctness_lemma : Constant.t option;
completeness_lemma : Constant.t option;
rect_lemma : Constant.t option;
rec_lemma : Constant.t option;
prop_lemma : Constant.t option;
sprop_lemma : Constant.t option;
is_general : bool;
}
val find_Function_infos : Constant.t -> function_info option
val find_Function_of_graph : inductive -> function_info option
(* WARNING: To be used just after the graph definition !!! *)
val add_Function : bool -> Constant.t -> unit
val update_Function : function_info -> unit
(** debugging *)
val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
val pr_table : Environ.env -> Evd.evar_map -> Pp.t
val observe_tac
: (Environ.env -> Evd.evar_map -> Pp.t)
-> Tacmach.tactic -> Tacmach.tactic
module New : sig
val observe_tac
: header:Pp.t
-> (Environ.env -> Evd.evar_map -> Pp.t)
-> unit Proofview.tactic -> unit Proofview.tactic
end
(* val function_debug : bool ref *)
val observe : Pp.t -> unit
val do_observe : unit -> bool
val do_rewrite_dependent : unit -> bool
(* To localize pb *)
exception Building_graph of exn
exception Defining_principle of exn
exception ToShow of exn
val is_strict_tcc : unit -> bool
val h_intros: Names.Id.t list -> Tacmach.tactic
val h_id : Names.Id.t
val hrec_id : Names.Id.t
val acc_inv_id : EConstr.constr Util.delayed
val ltof_ref : GlobRef.t Util.delayed
val well_founded_ltof : EConstr.constr Util.delayed
val acc_rel : EConstr.constr Util.delayed
val well_founded : EConstr.constr Util.delayed
val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference
val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
(Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t
val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t
type tcc_lemma_value =
| Undefined
| Value of Constr.t
| Not_needed
val funind_purify : ('a -> 'b) -> ('a -> 'b)
|
