blob: 69777da3e91ac1ec4e7f83c2850666e6d34a6f23 (
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
144
145
146
147
|
(*i $Id$ i*)
(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Proof_type
open Tacmach
open Hipattern
open Pattern
open Wcclausenv
open Tacticals
open Tactics
(*i*)
type leibniz_eq = {
eq : marked_term;
ind : marked_term;
rrec : marked_term option;
rect : marked_term option;
congr: marked_term;
sym : marked_term }
val eq : leibniz_eq
val eqT : leibniz_eq
val idT : leibniz_eq
val eq_pattern : unit -> constr_pattern
val eqT_pattern : unit -> constr_pattern
val idT_pattern : unit -> constr_pattern
val find_eq_pattern : sorts -> sorts -> constr
val general_rewrite_bindings : bool -> (constr * constr substitution) -> tactic
val general_rewrite : bool -> constr -> tactic
val rewriteLR_bindings : (constr * constr substitution) -> tactic
val h_rewriteLR_bindings : (constr * constr substitution) -> tactic
val rewriteRL_bindings : (constr * constr substitution) -> tactic
val h_rewriteRL_bindings : (constr * constr substitution) -> tactic
val rewriteLR : constr -> tactic
val h_rewriteLR : constr -> tactic
val rewriteRL : constr -> tactic
val h_rewriteRL : constr -> tactic
val conditional_rewrite :
bool -> tactic -> (constr * constr substitution) -> tactic
val general_rewrite_in :
bool -> identifier -> (constr * constr substitution) -> tactic
val conditional_rewrite_in :
bool -> identifier -> tactic -> (constr * constr substitution) -> tactic
(* usage : abstract_replace (eq,sym_eq) (eqt,sym_eqt) c2 c1 unsafe gl
eq,symeq : equality on Set and its symmetry theorem
eqt,sym_eqt : equality on Type and its symmetry theorem
c2 c1 : c1 is to be replaced by c2
unsafe : If true, do not check that c1 and c2 are convertible
gl : goal
*)
val abstract_replace :
constr * constr -> constr * constr -> constr -> constr -> bool -> tactic
(* Only for internal use *)
val unsafe_replace : constr -> constr -> tactic
val replace : constr -> constr -> tactic
val h_replace : constr -> constr -> tactic
type elimination_types =
| Set_Type
| Type_Type
| Set_SetorProp
| Type_SetorProp
(* necessary_elimination [sort_of_arity] [sort_of_goal] *)
val necessary_elimination : sorts -> sorts -> elimination_types
val discr : identifier -> tactic
val discrClause : clause -> tactic
val discrConcl : tactic
val discrHyp : identifier -> tactic
val discrEverywhere : tactic
val h_discrConcl : tactic
val h_discrHyp : identifier -> tactic
val h_discrConcl : tactic
val h_discr : tactic
val inj : identifier -> tactic
val h_injHyp : identifier -> tactic
val h_injConcl : tactic
val dEq : clause -> tactic
val dEqThen : (int -> tactic) -> clause -> tactic
val make_iterated_tuple :
env -> 'a evar_map -> (constr * constr) -> (constr * constr)
-> constr * constr * constr
val subst : constr -> clause -> tactic
val hypSubst : identifier -> clause -> tactic
val revSubst : constr -> clause -> tactic
val revHypSubst : identifier -> clause -> tactic
val discriminable : env -> 'a evar_map -> constr -> constr -> bool
(***************)
(* AutoRewrite *)
(***************)
(****Dealing with the rewriting rules****)
(*A rewriting is typically an equational constr with an orientation (true=LR
and false=RL)*)
type rewriting_rule = constr * bool
(*Adds a list of rules to the rule table*)
val add_list_rules : identifier -> rewriting_rule list -> unit
(****The tactic****)
(*For the Step options*)
type option_step =
| Solve
| Use
| All
(* the user can give a base either by a name of by its full definition
The definition is an Ast that will find its meaning only in the context
of a given goal *)
type hint_base =
| By_name of identifier
| Explicit of (Coqast.t * bool) list
val explicit_hint_base : goal sigma -> hint_base -> rewriting_rule list
(*AutoRewrite cannot be expressed with a combination of tacticals (due to the
options). So, we make it in a primitive way*)
val autorewrite :
hint_base list -> tactic list option -> option_step
-> tactic list option -> bool -> int -> tactic
|
