blob: 7cf088901e2a59c65e339f008ca1a2ec8deb2f51 (
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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Names
open Term
open Nametab
open Declare
open Library
open Libnames
open Nametab
open Tacexpr
open Vernacexpr
open Rawterm
open Topconstr
open Decl_kinds
open Redexpr
(*i*)
(*s Declaration functions. The following functions take ASTs,
transform them into [constr] and then call the corresponding
functions of [Declare]; they return an absolute reference to the
defined object *)
val get_declare_definition_hook : unit -> (Entries.definition_entry -> unit)
val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
val definition_message : identifier -> unit
val assumption_message : identifier -> unit
val declare_definition : identifier -> definition_kind ->
local_binder list -> red_expr option -> constr_expr ->
constr_expr option -> declaration_hook -> unit
val syntax_definition : identifier -> identifier list * constr_expr ->
bool -> bool -> unit
val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
Impargs.manual_explicitation list ->
bool (* implicit *) -> bool (* keep *) -> bool (* inline *) -> Names.variable located -> unit
val set_declare_assumption_hook : (types -> unit) -> unit
val declare_assumption : identifier located list ->
coercion_flag -> assumption_kind -> local_binder list -> constr_expr ->
bool -> bool -> bool -> unit
val declare_interning_data : 'a * Constrintern.implicits_env ->
string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type ->
'a list -> 'b list ->
Term.types list ->Impargs.manual_explicitation list list ->
'a list *
('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list *
Topconstr.scope_name option list))
list
val check_mutuality : Environ.env -> definition_object_kind ->
(identifier * types) list -> unit
val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) *
decl_notation) list -> bool -> unit
val declare_mutual_with_eliminations :
bool -> Entries.mutual_inductive_entry ->
(Impargs.manual_explicitation list *
Impargs.manual_explicitation list list) list ->
mutual_inductive
type fixpoint_kind =
| IsFixpoint of (identifier located option * recursion_order_expr) list
| IsCoFixpoint
type fixpoint_expr = {
fix_name : identifier;
fix_binders : local_binder list;
fix_body : constr_expr;
fix_type : constr_expr
}
val recursive_message : definition_object_kind ->
int array option -> identifier list -> Pp.std_ppcmds
val declare_fix : bool -> definition_object_kind -> identifier ->
constr -> types -> Impargs.manual_explicitation list -> global_reference
val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit
val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit
val build_scheme : (identifier located option * scheme ) list -> unit
val build_combined_scheme : identifier located -> identifier located list -> unit
val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
(* A hook start_proof calls on the type of the definition being started *)
val set_start_hook : (types -> unit) -> unit
val start_proof : identifier -> goal_kind -> types ->
?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit
val start_proof_com : goal_kind ->
(lident option * (local_binder list * constr_expr)) list ->
declaration_hook -> unit
(* A hook the next three functions pass to cook_proof *)
val set_save_hook : (Refiner.pftreestate -> unit) -> unit
(*s [save_named b] saves the current completed proof under the name it
was started; boolean [b] tells if the theorem is declared opaque; it
fails if the proof is not completed *)
val save_named : bool -> unit
(* [save_anonymous b name] behaves as [save_named] but declares the theorem
under the name [name] and respects the strength of the declaration *)
val save_anonymous : bool -> identifier -> unit
(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
declares the theorem under the name [name] and gives it the
strength [strength] *)
val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
(* [admit ()] aborts the current goal and save it as an assmumption *)
val admit : unit -> unit
(* [get_current_context ()] returns the evar context and env of the
current open proof if any, otherwise returns the empty evar context
and the current global env *)
val get_current_context : unit -> Evd.evar_map * Environ.env
|
