blob: 851c33e7a824920023546403996f5d9684a35a14 (
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
|
(************************************************************************)
(* 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 Names
open Util
open Term
open Proof_type
open Tacmach
open Genarg
open Tacexpr
open Rawterm
open Evd
open Clenv
open Termops
(*i*)
(* Tactics for the interpreter. They left a trace in the proof tree
when they are called. *)
(* Basic tactics *)
val h_intro_move : identifier option -> identifier move_location -> tactic
val h_intro : identifier -> tactic
val h_intros_until : quantified_hypothesis -> tactic
val h_assumption : tactic
val h_exact : constr -> tactic
val h_exact_no_check : constr -> tactic
val h_vm_cast_no_check : constr -> tactic
val h_apply : advanced_flag -> evars_flag ->
open_constr with_bindings list -> tactic
val h_elim : evars_flag -> constr with_ebindings ->
constr with_ebindings option -> tactic
val h_elim_type : constr -> tactic
val h_case : evars_flag -> constr with_ebindings -> tactic
val h_case_type : constr -> tactic
val h_mutual_fix : hidden_flag -> identifier -> int ->
(identifier * int * constr) list -> tactic
val h_fix : identifier option -> int -> tactic
val h_mutual_cofix : hidden_flag -> identifier ->
(identifier * constr) list -> tactic
val h_cofix : identifier option -> tactic
val h_cut : constr -> tactic
val h_generalize : constr list -> tactic
val h_generalize_gen : (constr with_occurrences * name) list -> tactic
val h_generalize_dep : constr -> tactic
val h_let_tac : letin_flag -> name -> constr ->
Tacticals.clause -> tactic
val h_instantiate : int -> Rawterm.rawconstr ->
(identifier * hyp_location_flag, unit) location -> tactic
(* Derived basic tactics *)
val h_simple_induction : quantified_hypothesis -> tactic
val h_simple_destruct : quantified_hypothesis -> tactic
val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic
val h_new_induction : evars_flag ->
constr with_ebindings induction_arg list -> constr with_ebindings option ->
intro_pattern_expr located option * intro_pattern_expr located option ->
Tacticals.clause option -> tactic
val h_new_destruct : evars_flag ->
constr with_ebindings induction_arg list -> constr with_ebindings option ->
intro_pattern_expr located option * intro_pattern_expr located option ->
Tacticals.clause option -> tactic
val h_induction_destruct : rec_flag -> evars_flag ->
(constr with_ebindings induction_arg list * constr with_ebindings option *
(intro_pattern_expr located option * intro_pattern_expr located option) *
Tacticals.clause option) list -> tactic
val h_specialize : int option -> constr with_ebindings -> tactic
val h_lapply : constr -> tactic
(* Automation tactic : see Auto *)
(* Context management *)
val h_clear : bool -> identifier list -> tactic
val h_clear_body : identifier list -> tactic
val h_move : bool -> identifier -> identifier move_location -> tactic
val h_rename : (identifier*identifier) list -> tactic
val h_revert : identifier list -> tactic
(* Constructors *)
val h_constructor : evars_flag -> int -> open_constr bindings -> tactic
val h_left : evars_flag -> open_constr bindings -> tactic
val h_right : evars_flag -> open_constr bindings -> tactic
val h_split : evars_flag -> open_constr bindings -> tactic
val h_one_constructor : int -> tactic
val h_simplest_left : tactic
val h_simplest_right : tactic
(* Conversion *)
val h_reduce : Redexpr.red_expr -> Tacticals.clause -> tactic
val h_change :
constr with_occurrences option -> constr -> Tacticals.clause -> tactic
(* Equivalence relations *)
val h_reflexivity : tactic
val h_symmetry : Tacticals.clause -> tactic
val h_transitivity : constr -> tactic
val h_simplest_apply : constr -> tactic
val h_simplest_eapply : constr -> tactic
val h_simplest_elim : constr -> tactic
val h_simplest_case : constr -> tactic
val h_intro_patterns : intro_pattern_expr located list -> tactic
|
