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
|
(************************************************************************)
(* * 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) *)
(************************************************************************)
open Names
open Environ
open EConstr
open Constrexpr
open Evd
open Genintern
open Tactypes
open Tacexpr
open Tacinterp
(** TODO: document and clean me! *)
type rewrite_attributes
val rewrite_attributes : rewrite_attributes Attributes.attribute
type unary_strategy =
Subterms | Subterm | Innermost | Outermost
| Bottomup | Topdown | Progress | Try | Any | Repeat
type binary_strategy =
| Compose | Choice
type ('constr,'redexpr) strategy_ast =
| StratId | StratFail | StratRefl
| StratUnary of unary_strategy * ('constr,'redexpr) strategy_ast
| StratBinary of binary_strategy
* ('constr,'redexpr) strategy_ast * ('constr,'redexpr) strategy_ast
| StratConstr of 'constr * bool
| StratTerms of 'constr list
| StratHints of bool * string
| StratEval of 'redexpr
| StratFold of 'constr
type rewrite_proof =
| RewPrf of constr * constr
| RewCast of Constr.cast_kind
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
type rewrite_result_info = {
rew_car : constr;
rew_from : constr;
rew_to : constr;
rew_prf : rewrite_proof;
rew_evars : evars;
}
type rewrite_result =
| Fail
| Identity
| Success of rewrite_result_info
type strategy
val strategy_of_ast : interp_sign -> (glob_constr_and_expr, glob_red_expr) strategy_ast -> strategy
val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) ->
('a, 'b) strategy_ast -> Pp.t
(** Entry point for user-level "rewrite_strat" *)
val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
(** Entry point for user-level "setoid_rewrite" *)
val cl_rewrite_clause :
interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) ->
bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic
val is_applied_rewrite_relation :
env -> evar_map -> rel_context -> constr -> types option
val declare_relation
: rewrite_attributes
-> ?binders:local_binder_expr list
-> constr_expr
-> constr_expr
-> Id.t
-> constr_expr option
-> constr_expr option
-> constr_expr option
-> unit
val add_setoid
: rewrite_attributes
-> local_binder_expr list
-> constr_expr
-> constr_expr
-> constr_expr
-> Id.t
-> unit
val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Declare.Proof.t
val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
val add_morphism
: rewrite_attributes
-> local_binder_expr list
-> constr_expr
-> constr_expr
-> Id.t
-> Declare.Proof.t
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
val get_symmetric_proof : env -> evar_map -> constr -> constr -> evar_map * constr
val get_transitive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
val default_morphism :
(types * constr option) option list * (types * types option) option ->
constr -> constr * constr
val setoid_symmetry : unit Proofview.tactic
val setoid_symmetry_in : Id.t -> unit Proofview.tactic
val setoid_reflexivity : unit Proofview.tactic
val setoid_transitivity : constr option -> unit Proofview.tactic
val apply_strategy :
strategy ->
Environ.env ->
Names.Id.Set.t ->
constr ->
bool * constr ->
evars -> rewrite_result
|
