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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
open Names
open Ltac_plugin
(* Names of variables to be cleared (automatic check: not a section var) *)
type ssrhyp = SsrHyp of Id.t Loc.located
(* Variant of the above *)
type ssrhyp_or_id = Hyp of ssrhyp | Id of ssrhyp
(* Variant of the above *)
type ssrhyps = ssrhyp list
(* Direction to be used for rewriting as in -> or rewrite flag *)
type ssrdir = Ssrmatching_plugin.Ssrmatching.ssrdir = L2R | R2L
(* simpl: "/=", cut: "//", simplcut: "//=" nop: commodity placeholder *)
type ssrsimpl = Simpl of int | Cut of int | SimplCut of int * int | Nop
(* modality for rewrite and do: ! ? *)
type ssrmmod = May | Must | Once
(* modality with a bound for rewrite and do: !n ?n *)
type ssrmult = int * ssrmmod
(** Occurrence switch {1 2}, all is Some(false,[]) *)
type ssrocc = (bool * int list) option
(* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
type ssrindex = int Misctypes.or_var
(* clear switch {H G} *)
type ssrclear = ssrhyps
(* Discharge occ switch (combined occurrence / clear switch) *)
type ssrdocc = ssrclear option * ssrocc
(* FIXME, make algebraic *)
type ssrtermkind = char
type ssrterm = ssrtermkind * Tacexpr.glob_constr_and_expr
type ssrview = ssrterm list
(* TODO
type id_mod = Hat | HatTilde | Sharp
*)
(* Only [One] forces an introduction, possibly reducing the goal. *)
type anon_iter =
| One
| Drop
| All
(* TODO
| Dependent (* fast mode *)
| UntilMark
| Temporary (* "+" *)
*)
type ssripat =
| IPatNoop
| IPatId of (*TODO id_mod option * *) Id.t
| IPatAnon of anon_iter (* inaccessible name *)
(* TODO | IPatClearMark *)
(* TODO | IPatDispatch of ssripatss (* /[..|..] *) *)
| IPatCase of (* ipats_mod option * *) ssripatss (* this is not equivalent to /case /[..|..] if there are already multiple goals *)
| IPatInj of ssripatss
| IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir
| IPatView of ssrterm list (* /view *)
| IPatClear of ssrclear (* {H1 H2} *)
| IPatSimpl of ssrsimpl
| IPatNewHidden of Id.t list
(* | IPatVarsForAbstract of Id.t list *)
and ssripats = ssripat list
and ssripatss = ssripats list
type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats
type ssrhpats_wtransp = bool * ssrhpats
(* tac => inpats *)
type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats
type ssrfwdid = Id.t
(** Binders (for fwd tactics) *)
type 'term ssrbind =
| Bvar of Name.t
| Bdecl of Name.t list * 'term
| Bdef of Name.t * 'term option * 'term
| Bstruct of Name.t
| Bcast of 'term
(* We use an intermediate structure to correctly render the binder list *)
(* abbreviations. We use a list of hints to extract the binders and *)
(* base term from a term, for the two first levels of representation of *)
(* of constr terms. *)
type ssrbindfmt =
| BFvar
| BFdecl of int (* #xs *)
| BFcast (* final cast *)
| BFdef (* has cast? *)
| BFrec of bool * bool (* has struct? * has cast? *)
type 'term ssrbindval = 'term ssrbind list * 'term
(** Forward chaining argument *)
(* There are three kinds of forward definitions: *)
(* - Hint: type only, cast to Type, may have proof hint. *)
(* - Have: type option + value, no space before type *)
(* - Pose: binders + value, space before binders. *)
type ssrfwdkind = FwdHint of string * bool | FwdHave | FwdPose
type ssrfwdfmt = ssrfwdkind * ssrbindfmt list
(* in *)
type ssrclseq = InGoal | InHyps
| InHypsGoal | InHypsSeqGoal | InSeqGoal | InHypsSeq | InAll | InAllHyps
type 'tac ssrhint = bool * 'tac option list
type 'tac fwdbinders =
bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint))
type clause =
(ssrclear * ((ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option) option)
type clauses = clause list * ssrclseq
type wgen =
(ssrclear *
((ssrhyp_or_id * string) *
Ssrmatching_plugin.Ssrmatching.cpattern option)
option)
type 'a ssrdoarg = ((ssrindex * ssrmmod) * 'a ssrhint) * clauses
type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option)
(* OOP : these are general shortcuts *)
type gist = Tacintern.glob_sign
type ist = Tacinterp.interp_sign
type goal = Goal.goal
type 'a sigma = 'a Evd.sigma
type v82tac = Tacmach.tactic
|
