blob: 580039afe596f1810462848e7c904d21cd241a5c (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Loc
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 located
type quantified_hypothesis =
| QAnonHyp of int located
| QNamedHyp of Id.t located
type bindings_r =
| QImplicitBindings of Constrexpr.constr_expr list
| QExplicitBindings of (quantified_hypothesis located or_anti * Constrexpr.constr_expr) located list
| QNoBindings
type bindings = bindings_r located
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 located or_anti
| QIntroFresh of Id.t located or_anti
| QIntroAnonymous
and intro_pattern_action_r =
| QIntroWildcard
| QIntroOrAndPattern of or_and_intro_pattern
| QIntroInjection of intro_pattern list located
(* | QIntroApplyOn of Empty.t (** Not implemented yet *) *)
| QIntroRewrite of bool
and or_and_intro_pattern_r =
| QIntroOrPattern of intro_pattern list located list
| QIntroAndPattern of intro_pattern list located
and intro_pattern = intro_pattern_r located
and intro_pattern_naming = intro_pattern_naming_r located
and intro_pattern_action = intro_pattern_action_r located
and or_and_intro_pattern = or_and_intro_pattern_r located
type occurrences_r =
| QAllOccurrences
| QAllOccurrencesBut of int located or_anti list
| QNoOccurrences
| QOnlyOccurrences of int located or_anti list
type occurrences = occurrences_r located
type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_flag
type clause_r =
{ q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
type clause = clause_r located
type constr_with_bindings = (Constrexpr.constr_expr * bindings) located
type destruction_arg_r =
| QElimOnConstr of constr_with_bindings
| QElimOnIdent of Id.t located
| QElimOnAnonHyp of int located
type destruction_arg = destruction_arg_r located
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 located
type multi_r =
| QPrecisely of int located
| QUpTo of int located
| QRepeatStar
| QRepeatPlus
type multi = multi_r located
type rewriting_r = {
rew_orient : bool option located;
rew_repeat : multi;
rew_equatn : constr_with_bindings;
}
type rewriting = rewriting_r located
type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) option
type dispatch = dispatch_r located
type red_flag_r =
| QBeta
| QIota
| QMatch
| QFix
| QCofix
| QZeta
| QConst of Libnames.reference or_anti list located
| QDeltaBut of Libnames.reference or_anti list located
type red_flag = red_flag_r located
type strategy_flag = red_flag list located
type constr_match_branch_r =
| QConstrMatchPattern of Constrexpr.constr_expr * raw_tacexpr
| QConstrMatchContext of Id.t option * Constrexpr.constr_expr * raw_tacexpr
type constr_match_branch = constr_match_branch_r located
type constr_matching = constr_match_branch list located
type hintdb_r =
| QHintAll
| QHintDbs of Id.t located or_anti list
type hintdb = hintdb_r located
type move_location_r =
| QMoveAfter of Id.t located or_anti
| QMoveBefore of Id.t located or_anti
| QMoveFirst
| QMoveLast
type move_location = move_location_r located
type pose = (Id.t located or_anti option * Constrexpr.constr_expr) located
|
