blob: 7b63099c741178450c8b52787d2208b3f96e1146 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*i*)
open Util
open Names
open Term
open Sign
open Evd
open Environ
open Proof_type
open Tacmach
open Hipattern
open Pattern
open Tacticals
open Tactics
open Tacexpr
open Termops
open Rawterm
open Genarg
(*i*)
type orientation = bool
type conditions =
| Naive (* Only try the first occurence of the lemma (default) *)
| FirstSolved (* Use the first match whose side-conditions are solved *)
| AllMatches (* Rewrite all matches whose side-conditions are solved *)
val general_rewrite_bindings :
orientation -> occurrences -> ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
val general_rewrite :
orientation -> occurrences -> ?tac:(tactic * conditions) -> constr -> tactic
(* Equivalent to [general_rewrite l2r] *)
val rewriteLR : ?tac:(tactic * conditions) -> constr -> tactic
val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
val register_general_rewrite_clause :
(identifier option -> orientation ->
occurrences -> open_constr with_bindings -> new_goals:constr list -> tactic) -> unit
val register_is_applied_rewrite_relation : (env -> evar_defs -> rel_context -> constr -> open_constr option) -> unit
val general_rewrite_ebindings_clause : identifier option ->
orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic
val general_rewrite_bindings_in :
orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_in :
orientation -> occurrences -> ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic
val general_multi_rewrite :
orientation -> evars_flag -> ?tac:(tactic * conditions) -> open_constr with_bindings -> clause -> tactic
val general_multi_multi_rewrite :
evars_flag -> (bool * multi * open_constr with_bindings) list -> clause ->
(tactic * conditions) option -> tactic
val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
val replace : constr -> constr -> tactic
val replace_in : identifier -> constr -> constr -> tactic
val replace_by : constr -> constr -> tactic -> tactic
val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
val discr : evars_flag -> constr with_ebindings -> tactic
val discrConcl : tactic
val discrClause : evars_flag -> clause -> tactic
val discrHyp : identifier -> tactic
val discrEverywhere : evars_flag -> tactic
val discr_tac : evars_flag ->
constr with_ebindings induction_arg option -> tactic
val inj : intro_pattern_expr located list -> evars_flag ->
constr with_ebindings -> tactic
val injClause : intro_pattern_expr located list -> evars_flag ->
constr with_ebindings induction_arg option -> tactic
val injHyp : identifier -> tactic
val injConcl : tactic
val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic
val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic
val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
(* The family cutRewriteIn expect an equality statement *)
val cutRewriteInHyp : bool -> types -> identifier -> tactic
val cutRewriteInConcl : bool -> constr -> tactic
(* The family rewriteIn expect the proof of an equality *)
val rewriteInHyp : bool -> constr -> identifier -> tactic
val rewriteInConcl : bool -> constr -> tactic
(* Expect the proof of an equality; fails with raw internal errors *)
val substClause : bool -> constr -> identifier option -> tactic
(*
(* [substHypInConcl l2r id] is obsolete: use [rewriteInConcl l2r (mkVar id)] *)
val substHypInConcl : bool -> identifier -> tactic
(* [substConcl] is an obsolete synonym for [cutRewriteInConcl] *)
val substConcl : bool -> constr -> tactic
(* [substHyp] is an obsolete synonym of [cutRewriteInHyp] *)
val substHyp : bool -> types -> identifier -> tactic
*)
(* Obsolete, use [rewriteInConcl lr (mkVar id)] in concl
or [rewriteInHyp lr (mkVar id) (Some hyp)] in hyp
(which, if they fail, raise only UserError, not PatternMatchingFailure)
or [substClause lr (mkVar id) None]
or [substClause lr (mkVar id) (Some hyp)]
[val hypSubst_LR : identifier -> clause -> tactic]
[val hypSubst_RL : identifier -> clause -> tactic]
*)
val discriminable : env -> evar_map -> constr -> constr -> bool
val injectable : env -> evar_map -> constr -> constr -> bool
(* Subst *)
val unfold_body : identifier -> tactic
val subst : identifier list -> tactic
val subst_all : ?strict:bool -> tactic
(* Replace term *)
(* [replace_multi_term dir_opt c cl]
perfoms replacement of [c] by the first value found in context
(according to [dir] if given to get the rewrite direction) in the clause [cl]
*)
val replace_multi_term : bool option -> constr -> clause -> tactic
|
