blob: 86ab39dfffb257796612838202904ce024b98c6a (
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
|
(***********************************************************************)
(* 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 Proof_type
open Tacmach
(*i*)
(* Registered tactics. *)
val v_absurd : tactic_arg list -> tactic
val v_contradiction : tactic_arg list -> tactic
val v_reflexivity : tactic_arg list -> tactic
val v_symmetry : tactic_arg list -> tactic
val v_transitivity : tactic_arg list -> tactic
val v_intro : tactic_arg list -> tactic
val v_introsUntil : tactic_arg list -> tactic
(*i val v_tclIDTAC : tactic_arg list -> tactic i*)
val v_assumption : tactic_arg list -> tactic
val v_exact : tactic_arg list -> tactic
val v_reduce : tactic_arg list -> tactic
val v_constructor : tactic_arg list -> tactic
val v_left : tactic_arg list -> tactic
val v_right : tactic_arg list -> tactic
val v_split : tactic_arg list -> tactic
val v_clear : tactic_arg list -> tactic
val v_clear_body : tactic_arg list -> tactic
val v_move : tactic_arg list -> tactic
val v_move_dep : tactic_arg list -> tactic
val v_apply : tactic_arg list -> tactic
val v_cutAndResolve : tactic_arg list -> tactic
val v_cut : tactic_arg list -> tactic
val v_truecut : tactic_arg list -> tactic
val v_lettac : tactic_arg list -> tactic
val v_generalize : tactic_arg list -> tactic
val v_generalize_dep : tactic_arg list -> tactic
val v_specialize : tactic_arg list -> tactic
val v_elim : tactic_arg list -> tactic
val v_elimType : tactic_arg list -> tactic
val v_induction : tactic_arg list -> tactic
(*i val v_new_induction : tactic_arg list -> tactic i*)
val v_case : tactic_arg list -> tactic
val v_caseType : tactic_arg list -> tactic
val v_destruct : tactic_arg list -> tactic
(*i val v_new_destruct : tactic_arg list -> tactic i*)
val v_fix : tactic_arg list -> tactic
val v_cofix : tactic_arg list -> tactic
val vernac_instantiate : tactic_arg list -> tactic
|
