blob: 40b6573a15d2510abb68eb61db7cd335af40bb7b (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
open Term
open Environ
open EConstr
open Evd
open Proof_type
open Redexpr
open Pattern
open Locus
(** Operations for handling terms under a local typing context. *)
type 'a sigma = 'a Evd.sigma;;
type tactic = Proof_type.tactic;;
val sig_it : 'a sigma -> 'a
val project : goal sigma -> evar_map
val re_sig : 'a -> evar_map -> 'a sigma
val unpackage : 'a sigma -> evar_map ref * 'a
val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
val pf_hyps : goal sigma -> named_context
(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*)
val pf_hyps_types : goal sigma -> (Id.t * types) list
val pf_nth_hyp_id : goal sigma -> int -> Id.t
val pf_last_hyp : goal sigma -> named_declaration
val pf_ids_of_hyps : goal sigma -> Id.t list
val pf_global : goal sigma -> Id.t -> constr
val pf_unsafe_type_of : goal sigma -> constr -> types
val pf_type_of : goal sigma -> constr -> evar_map * types
val pf_hnf_type_of : goal sigma -> constr -> types
val pf_get_hyp : goal sigma -> Id.t -> named_declaration
val pf_get_hyp_typ : goal sigma -> Id.t -> types
val pf_get_new_id : Id.t -> goal sigma -> Id.t
val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) ->
goal sigma -> 'a -> goal sigma * 'b
val pf_reduce :
(env -> evar_map -> constr -> constr) ->
goal sigma -> constr -> constr
val pf_e_reduce :
(env -> evar_map -> constr -> evar_map * constr) ->
goal sigma -> constr -> evar_map * constr
val pf_whd_all : goal sigma -> constr -> constr
val pf_hnf_constr : goal sigma -> constr -> constr
val pf_nf : goal sigma -> constr -> constr
val pf_nf_betaiota : goal sigma -> constr -> constr
val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types
val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types
val pf_compute : goal sigma -> constr -> constr
val pf_unfoldn : (occurrences * evaluable_global_reference) list
-> goal sigma -> constr -> constr
val pf_const_value : goal sigma -> pconstant -> constr
val pf_conv_x : goal sigma -> constr -> constr -> bool
val pf_conv_x_leq : goal sigma -> constr -> constr -> bool
val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map
val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
(** {6 The most primitive tactics. } *)
val refiner : rule -> tactic
val internal_cut_no_check : bool -> Id.t -> types -> tactic
val refine_no_check : constr -> tactic
(** {6 The most primitive tactics with consistency and type checking } *)
val internal_cut : bool -> Id.t -> types -> tactic
val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : goal sigma -> Pp.t
val pr_glls : goal list sigma -> Pp.t
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
val pf_global : identifier -> 'a Proofview.Goal.t -> Globnames.global_reference
(** FIXME: encapsulate the level in an existential type. *)
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
val project : 'a Proofview.Goal.t -> Evd.evar_map
val pf_env : 'a Proofview.Goal.t -> Environ.env
val pf_concl : 'a Proofview.Goal.t -> types
(** WRONG: To be avoided at all costs, it typechecks the term entirely but
forgets the universe constraints necessary to retypecheck it *)
val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types
(** This function does no type inference and expects an already well-typed term.
It recomputes its type in the fastest way possible (no conversion is ever involved) *)
val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types
(** This function entirely type-checks the term and computes its type
and the implied universe constraints. *)
val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types
val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool
val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier
val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration
val pf_get_hyp_typ : identifier -> 'a Proofview.Goal.t -> types
val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration
val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types
val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
val pf_compute : 'a Proofview.Goal.t -> constr -> constr
val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
end
|
