blob: 47ec783742ff4aebc164281dbbb4d54011697daf (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*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
open Tacexpr
open Rawterm
(*i*)
val find_eq_pattern : sorts -> sorts -> constr
val general_rewrite_bindings : bool -> constr with_bindings -> tactic
val general_rewrite : bool -> constr -> tactic
val rewriteLR_bindings : constr with_bindings -> tactic
val rewriteRL_bindings : constr with_bindings -> tactic
val rewriteLR : constr -> tactic
val rewriteRL : constr -> tactic
val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
val general_rewrite_in : bool -> identifier -> constr with_bindings -> tactic
val conditional_rewrite_in :
bool -> identifier -> tactic -> constr with_bindings -> 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
val 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 discr_tac : identifier option -> tactic
val inj : identifier -> tactic
val injClause : clause -> tactic
val dEq : clause -> tactic
val dEqThen : (int -> tactic) -> clause -> tactic
val make_iterated_tuple :
env -> evar_map -> (constr * constr) -> (constr * constr)
-> constr * constr * constr
val substHypInConcl : bool -> identifier -> tactic
val substConcl : bool -> constr -> tactic
val substHyp : bool -> constr -> identifier -> tactic
val hypSubst_LR : identifier -> clause -> tactic
val hypSubst_RL : identifier -> clause -> tactic
val discriminable : env -> 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
|
