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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* This module implements the abstract interface to goals *)
type goal
(* spiwack: this primitive is not extremely brilliant. It may be a good
idea to define goals and proof views in the same file to avoid this
sort of communication pipes. But I find it heavy. *)
val build : Evd.evar -> goal
(* Gives a unique identifier to each goal. The identifier is
guaranteed to contain no space. *)
val uid : goal -> string
(* Returns the goal (even if it has been partially solved)
corresponding to a unique identifier obtained by {!uid}. *)
val get_by_uid : string -> goal
(* Debugging help *)
val pr_goal : goal -> Pp.std_ppcmds
val goal_ident : Evd.evar_map -> goal -> Names.Id.t
val dependent_goal_ident : Evd.evar_map -> goal -> Names.Id.t
(* [advance sigma g] returns [Some g'] if [g'] is undefined and
is the current avatar of [g] (for instance [g] was changed by [clear]
into [g']). It returns [None] if [g] has been (partially) solved. *)
val advance : Evd.evar_map -> goal -> goal option
val solution : Evd.evar_map -> goal -> Term.constr option
(* Equality function on goals. Return [true] if all of its hypotheses
and conclusion are equal. *)
val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
(* [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
where [u] is composed of the unifiable goals, i.e. the goals on
whose definition other goals of [l] depend, and [n] are the
non-unifiable goals. *)
val partition_unifiable : Evd.evar_map -> goal list -> goal list * goal list
(* Layer to implement v8.2 tactic engine ontop of the new architecture.
Types are different from what they used to be due to a change of the
internal types. *)
module V82 : sig
(* Old style env primitive *)
val env : Evd.evar_map -> goal -> Environ.env
(* same as [env], but ensures that existential variables are
normalised *)
val nf_env : Evd.evar_map -> goal -> Environ.env
(* Old style hyps primitive *)
val hyps : Evd.evar_map -> goal -> Environ.named_context_val
(* same as [hyps], but ensures that existential variables are
normalised. *)
val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
(* Access to ".evar_concl" *)
val concl : Evd.evar_map -> goal -> Term.constr
(* same as [concl] but ensures that existential variables are
normalised. *)
val nf_concl : Evd.evar_map -> goal -> Term.constr
(* Access to ".evar_extra" *)
val extra : Evd.evar_map -> goal -> Evd.Store.t
(* Old style filtered_context primitive *)
val filtered_context : Evd.evar_map -> goal -> Context.named_context
(* Old style mk_goal primitive, returns a new goal with corresponding
hypotheses and conclusion, together with a term which is precisely
the evar corresponding to the goal, and an updated evar_map. *)
val mk_goal : Evd.evar_map ->
Environ.named_context_val ->
Term.constr ->
Evd.Store.t ->
goal * Term.constr * Evd.evar_map
(* Creates a dummy [goal sigma] for use in auto *)
val dummy_goal : goal Evd.sigma
(* Makes a goal out of an evar *)
(* spiwack: used by [Proofview.init], not entirely clean probably, but it is
the only way I could think of to preserve compatibility with previous Coq
stuff. *)
val build : Evd.evar -> goal
(* Instantiates a goal with an open term *)
val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
(* Instantiates a goal with an open term, reusing name of goal for
second goal *)
val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
(* Principal part of the weak-progress tactical *)
val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
(* Principal part of the progress tactical *)
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
(* Principal part of tclNOTSAMEGOAL *)
val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
(* Used for congruence closure *)
val new_goal_with : Evd.evar_map -> goal -> Context.named_context -> goal Evd.sigma
(* Used by the compatibility layer and typeclasses *)
val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
(* Goal represented as a type, doesn't take into account section variables *)
val abstract_type : Evd.evar_map -> goal -> Term.types
end
(*** Goal tactics. DEPRECATED. ***)
(* Goal sensitive values *)
type +'a sensitive
(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
val eval :
'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
'a * Evd.evar_map
(* [enter] combines [env], [defs], [hyps] and [concl] in a single
primitive. *)
val enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive
val nf_enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive
|
