blob: 3d6a08b6b04725cae85202ef6faed2c96033bac1 (
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
|
(************************************************************************)
(* 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: equality.mli 9195 2006-10-01 09:41:57Z herbelin $ i*)
(*i*)
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 Rawterm
open Genarg
(*i*)
val general_rewrite_bindings : bool -> constr with_bindings -> tactic
val general_rewrite : bool -> constr -> tactic
(* Obsolete, use [general_rewrite_bindings l2r]
[val rewriteLR_bindings : constr with_bindings -> tactic]
[val rewriteRL_bindings : constr with_bindings -> tactic]
*)
(* Equivalent to [general_rewrite l2r] *)
val rewriteLR : constr -> tactic
val rewriteRL : constr -> tactic
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
val general_rewrite_bindings_in :
bool -> identifier -> constr with_bindings -> tactic
val general_rewrite_in :
bool -> identifier -> constr -> tactic
val general_multi_rewrite :
bool -> constr with_bindings -> clause -> tactic
val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
val conditional_rewrite_in :
bool -> identifier -> tactic -> constr with_bindings -> 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 : identifier -> tactic
val discrConcl : tactic
val discrClause : clause -> tactic
val discrHyp : identifier -> tactic
val discrEverywhere : tactic
val discr_tac : quantified_hypothesis option -> tactic
val inj : intro_pattern_expr list -> identifier -> tactic
val injClause : intro_pattern_expr list -> quantified_hypothesis option ->
tactic
val dEq : quantified_hypothesis option -> tactic
val dEqThen : (int -> tactic) -> quantified_hypothesis 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
(* Subst *)
val unfold_body : identifier -> tactic
val subst : identifier list -> tactic
val subst_all : 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
|
