blob: 098e9272197dfbbae9d3b5dab0b7a6dced359477 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i*)
open Pp
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 Glob_term
open Genarg
open Ind_tables
open Locus
open Misctypes
(*i*)
type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
type freeze_evars_flag = bool (* true = don't instantiate existing evars *)
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 -> freeze_evars_flag -> dep_proof_flag ->
?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
val general_rewrite :
orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?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 -> constr with_bindings -> new_goals:constr list -> tactic) -> unit
val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit
val general_rewrite_ebindings_clause : identifier option ->
orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_bindings_in :
orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(tactic * conditions) ->
identifier -> constr with_bindings -> evars_flag -> tactic
val general_rewrite_in :
orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic
val general_multi_rewrite :
orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic
type delayed_open_constr_with_bindings =
env -> evar_map -> evar_map * constr with_bindings
val general_multi_multi_rewrite :
evars_flag -> (bool * multi * delayed_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_bindings -> 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_bindings induction_arg option -> tactic
val inj : intro_pattern_expr located list -> evars_flag ->
constr with_bindings -> tactic
val injClause : intro_pattern_expr located list -> evars_flag ->
constr with_bindings induction_arg option -> tactic
val injHyp : identifier -> tactic
val injConcl : tactic
val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic
val dEqThen : evars_flag -> (int -> tactic) -> constr with_bindings 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
val discriminable : env -> evar_map -> constr -> constr -> bool
val injectable : env -> evar_map -> constr -> constr -> bool
(* Subst *)
val unfold_body : identifier -> tactic
type subst_tactic_flags = {
only_leibniz : bool;
rewrite_dependent_proof : bool
}
val subst_gen : bool -> identifier list -> tactic
val subst : identifier list -> tactic
val subst_all : ?flags:subst_tactic_flags -> 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
val set_eq_dec_scheme_kind : mutual scheme_kind -> unit
|
