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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
(* This file implements:
- the [=>] tactical
- the [:] pseudo-tactical for move, case, elim and abstract
Putting these two features in the same file lets one hide much of the
interaction between [tac E:] and [=>] ([E] has to be processed by [=>],
not by [:]
*)
open Ssrast
(* Atomic operations for the IPat machine. Use this if you are "patching" an
* ipat written by the user, since patching it at he AST level and then
* compiling it may have tricky effects, eg adding a clear in front of a view
* also has the effect of disposing the view (the compilation phase takes care
* of this, by using the compiled ipats you can be more precise *)
type ssriop =
| IOpId of Names.Id.t
| IOpDrop
| IOpTemporay
| IOpInaccessible of string option
| IOpInaccessibleAll
| IOpAbstractVars of Names.Id.t list
| IOpFastNondep
| IOpInj of ssriops list
| IOpDispatchBlock of id_block
| IOpDispatchBranches of ssriops list
| IOpCaseBlock of id_block
| IOpCaseBranches of ssriops list
| IOpRewrite of ssrocc * ssrdir
| IOpView of ssrclear option * ssrview (* extra clears to be performed *)
| IOpClear of ssrclear * ssrhyp option
| IOpSimpl of ssrsimpl
| IOpEqGen of unit Proofview.tactic (* generation of eqn *)
| IOpNoop
and ssriops = ssriop list
val tclCompileIPats : ssripats -> ssriops
(* The => tactical *)
val tclIPAT : ssriops -> unit Proofview.tactic
(* As above but with the SSR exception: first case is dispatch *)
val tclIPATssr : ssripats -> unit Proofview.tactic
(* Wrappers to deal with : and eqn generation/naming:
[tac E: gens => ipats]
where [E] is injected into [ipats] (at the right place) and [gens] are
generalized before calling [tac] *)
val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrsmovetac : unit Proofview.tactic
val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrselimtoptac : unit Proofview.tactic
val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic
val ssrscasetoptac : unit Proofview.tactic
(* The implementation of abstract: is half here, for the [[: var ]]
* ipat, and in ssrfwd for the integration with [have] *)
val ssrabstract : ssrdgens -> unit Proofview.tactic
module Internal : sig
val examine_abstract :
Environ.env -> Evd.evar_map -> EConstr.t -> Evd.evar_map * (EConstr.types * EConstr.t array)
val find_abstract_proof :
Environ.env -> Evd.evar_map -> bool -> EConstr.constr -> Evar.t
end
|
