blob: aeaae6b4efe9ceeee98be2815c66f9879f33ee6d (
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-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
(*i*)
open Names
open Term
open Sign
open Tacmach
open Proof_type
open Clenv
open Reduction
open Pattern
open Wcclausenv
(*i*)
(* Tacticals i.e. functions from tactics to tactics. *)
val tclIDTAC : tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
val tclTHENL : tactic -> tactic -> tactic
val tclTHENS : tactic -> tactic list -> tactic
val tclTHENSi : tactic -> tactic list -> (int -> tactic) -> tactic
val tclREPEAT : tactic -> tactic
val tclFIRST : tactic list -> tactic
val tclTRY : tactic -> tactic
val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
val tclFAIL : int -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclNTH_HYP : int -> (constr -> tactic) -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
val tclLAST_HYP : (constr -> tactic) -> tactic
val tclTRY_sign : (constr -> tactic) -> named_context -> tactic
val tclTRY_HYPS : (constr -> tactic) -> tactic
(*i
val dyn_tclIDTAC : tactic_arg list -> tactic
val dyn_tclFAIL : tactic_arg list -> tactic
i*)
(*s Clause tacticals. *)
type clause = identifier option
val nth_clause : int -> goal sigma -> clause
val clause_type : clause -> goal sigma -> constr
(*i
val matches : goal sigma -> constr -> marked_term -> bool
val dest_match : goal sigma -> constr -> marked_term -> constr list
i*)
val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
val allHyps : goal sigma -> clause list
val afterHyp : identifier -> goal sigma -> clause list
val lastHyp : goal sigma -> clause list
val nLastHyps : int -> goal sigma -> clause list
val allClauses : goal sigma -> clause list
val onCL : (goal sigma -> clause list) ->
(clause list -> tactic) -> tactic
val tryAllHyps : (clause -> tactic) -> tactic
val tryAllClauses : (clause -> tactic) -> tactic
val onAllClauses : (clause -> tactic) -> tactic
val onClause : (clause -> tactic) -> clause -> tactic
val onAllClausesLR : (clause -> tactic) -> tactic
val onLastHyp : (clause -> tactic) -> tactic
val onNthLastHyp : int -> (clause -> tactic) -> tactic
val onNLastHyps : int -> (clause -> tactic) -> tactic
val clauseTacThen : (clause -> tactic) -> tactic -> clause -> tactic
val if_tac : (goal sigma -> bool) -> tactic -> (tactic) -> tactic
val ifOnClause :
(clause * constr -> bool) -> (clause -> tactic) -> (clause -> tactic) ->
clause -> tactic
(* [ConclPattern concl pat tacast]:
if the term concl matches the pattern pat, (in sense of
[Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
right values to build a tactic *)
val conclPattern : constr -> constr_pattern -> Coqast.t -> tactic
(*s Elimination tacticals. *)
type branch_args = {
ity : inductive; (* the type we were eliminating on *)
largs : constr list; (* its arguments *)
branchnum : int; (* the branch number *)
pred : constr; (* the predicate we used *)
nassums : int; (* the number of assumptions to be introduced *)
branchsign : bool list } (* the signature of the branch.
true=recursive argument, false=constant *)
type branch_assumptions = {
ba : branch_args; (* the branch args *)
assums : identifier list; (* the list of assumptions introduced *)
cargs : identifier list; (* the constructor arguments *)
constargs : identifier list; (* the CONSTANT constructor arguments *)
recargs : identifier list; (* the RECURSIVE constructor arguments *)
indargs : identifier list} (* the inductive arguments *)
val sort_of_goal : goal sigma -> sorts
(*i val suff : goal sigma -> constr -> string i*)
val general_elim_then_using :
constr -> (inductive -> int -> bool list) ->
(branch_args -> tactic) -> constr option ->
(arg_bindings * arg_bindings) -> constr -> tactic
val elimination_then_using :
(branch_args -> tactic) -> constr option ->
(arg_bindings * arg_bindings) -> constr -> tactic
val elimination_then :
(branch_args -> tactic) ->
(arg_bindings * arg_bindings) -> constr -> tactic
val case_then_using :
(branch_args -> tactic) ->
constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
val case_nodep_then_using :
(branch_args -> tactic) ->
constr option -> (arg_bindings * arg_bindings) -> constr -> tactic
val simple_elimination_then :
(branch_args -> tactic) -> constr -> tactic
val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic
val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic
|
