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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Tac2expr
(** Quoted variants of Ltac syntactic categories. Contrarily to the former, they
sometimes allow anti-quotations. Used for notation scopes. *)
type 'a or_anti =
| QExpr of 'a
| QAnti of Id.t CAst.t
type reference_r =
| QReference of Libnames.qualid
| QHypothesis of Id.t
type reference = reference_r CAst.t
type quantified_hypothesis =
| QAnonHyp of int CAst.t
| QNamedHyp of Id.t CAst.t
type bindings_r =
| QImplicitBindings of Constrexpr.constr_expr list
| QExplicitBindings of (quantified_hypothesis CAst.t or_anti * Constrexpr.constr_expr) CAst.t list
| QNoBindings
type bindings = bindings_r CAst.t
type intro_pattern_r =
| QIntroForthcoming of bool
| QIntroNaming of intro_pattern_naming
| QIntroAction of intro_pattern_action
and intro_pattern_naming_r =
| QIntroIdentifier of Id.t CAst.t or_anti
| QIntroFresh of Id.t CAst.t or_anti
| QIntroAnonymous
and intro_pattern_action_r =
| QIntroWildcard
| QIntroOrAndPattern of or_and_intro_pattern
| QIntroInjection of intro_pattern list CAst.t
(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
| QIntroRewrite of bool
and or_and_intro_pattern_r =
| QIntroOrPattern of intro_pattern list CAst.t list
| QIntroAndPattern of intro_pattern list CAst.t
and intro_pattern = intro_pattern_r CAst.t
and intro_pattern_naming = intro_pattern_naming_r CAst.t
and intro_pattern_action = intro_pattern_action_r CAst.t
and or_and_intro_pattern = or_and_intro_pattern_r CAst.t
type occurrences_r =
| QAllOccurrences
| QAllOccurrencesBut of int CAst.t or_anti list
| QNoOccurrences
| QOnlyOccurrences of int CAst.t or_anti list
type occurrences = occurrences_r CAst.t
type hyp_location = (occurrences * Id.t CAst.t or_anti) * Locus.hyp_location_flag
type clause_r =
{ q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
type clause = clause_r CAst.t
type constr_with_bindings = (Constrexpr.constr_expr * bindings) CAst.t
type destruction_arg_r =
| QElimOnConstr of constr_with_bindings
| QElimOnIdent of Id.t CAst.t
| QElimOnAnonHyp of int CAst.t
type destruction_arg = destruction_arg_r CAst.t
type induction_clause_r = {
indcl_arg : destruction_arg;
indcl_eqn : intro_pattern_naming option;
indcl_as : or_and_intro_pattern option;
indcl_in : clause option;
}
type induction_clause = induction_clause_r CAst.t
type conversion_r =
| QConvert of Constrexpr.constr_expr
| QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr
type conversion = conversion_r CAst.t
type multi_r =
| QPrecisely of int CAst.t
| QUpTo of int CAst.t
| QRepeatStar
| QRepeatPlus
type multi = multi_r CAst.t
type rewriting_r = {
rew_orient : bool option CAst.t;
rew_repeat : multi;
rew_equatn : constr_with_bindings;
}
type rewriting = rewriting_r CAst.t
type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) option
type dispatch = dispatch_r CAst.t
type red_flag_r =
| QBeta
| QIota
| QMatch
| QFix
| QCofix
| QZeta
| QConst of reference or_anti list CAst.t
| QDeltaBut of reference or_anti list CAst.t
type red_flag = red_flag_r CAst.t
type strategy_flag = red_flag list CAst.t
type constr_match_pattern_r =
| QConstrMatchPattern of Constrexpr.constr_expr
| QConstrMatchContext of Id.t option * Constrexpr.constr_expr
type constr_match_pattern = constr_match_pattern_r CAst.t
type constr_match_branch = (constr_match_pattern * raw_tacexpr) CAst.t
type constr_matching = constr_match_branch list CAst.t
type goal_match_pattern_r = {
q_goal_match_concl : constr_match_pattern;
q_goal_match_hyps : (Names.lname * constr_match_pattern) list;
}
type goal_match_pattern = goal_match_pattern_r CAst.t
type goal_match_branch = (goal_match_pattern * raw_tacexpr) CAst.t
type goal_matching = goal_match_branch list CAst.t
type hintdb_r =
| QHintAll
| QHintDbs of Id.t CAst.t or_anti list
type hintdb = hintdb_r CAst.t
type move_location_r =
| QMoveAfter of Id.t CAst.t or_anti
| QMoveBefore of Id.t CAst.t or_anti
| QMoveFirst
| QMoveLast
type move_location = move_location_r CAst.t
type pose = (Id.t CAst.t or_anti option * Constrexpr.constr_expr) CAst.t
type assertion_r =
| QAssertType of intro_pattern option * Constrexpr.constr_expr * raw_tacexpr option
| QAssertValue of Id.t CAst.t or_anti * Constrexpr.constr_expr
type assertion = assertion_r CAst.t
|
