1 (* GENERATED FILE, DO NOT EDIT. STAMP:Sun Jun 8 15:54:21 CEST 2008 *)
2 val absurd : term:Cic.term -> ProofEngineTypes.tactic
3 val apply : term:Cic.term -> ProofEngineTypes.tactic
7 params:Auto.auto_params ->
8 universe:Universe.universe -> ProofEngineTypes.tactic
9 val assumption : ProofEngineTypes.tactic
12 params:Auto.auto_params ->
13 universe:Universe.universe -> ProofEngineTypes.tactic
16 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
17 Cic.term -> ProofEngineTypes.tactic
20 pattern:ProofEngineTypes.lazy_pattern ->
21 Cic.lazy_term -> ProofEngineTypes.tactic
22 val clear : hyps:string list -> ProofEngineTypes.tactic
23 val clearbody : hyp:string -> ProofEngineTypes.tactic
24 val constructor : n:int -> ProofEngineTypes.tactic
25 val contradiction : ProofEngineTypes.tactic
27 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
28 Cic.term -> ProofEngineTypes.tactic
31 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
32 unit -> ProofEngineTypes.tactic
35 params:Auto.auto_params ->
36 universe:Universe.universe -> ProofEngineTypes.tactic
37 val destruct : Cic.term list option -> ProofEngineTypes.tactic
39 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
42 ?pattern:ProofEngineTypes.lazy_pattern ->
43 Cic.term -> ProofEngineTypes.tactic
44 val elim_intros_simpl :
45 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
48 ?pattern:ProofEngineTypes.lazy_pattern ->
49 Cic.term -> ProofEngineTypes.tactic
51 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
52 ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
53 val exact : term:Cic.term -> ProofEngineTypes.tactic
54 val exists : ProofEngineTypes.tactic
55 val fail : Tacticals.tactic
57 reduction:ProofEngineTypes.lazy_reduction ->
59 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
60 val fourier : ProofEngineTypes.tactic
62 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
63 dbd:HSql.dbd -> string -> ProofEngineTypes.tactic
65 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
66 ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
67 val id : Tacticals.tactic
70 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
71 unit -> ProofEngineTypes.tactic
72 val inversion : term:Cic.term -> ProofEngineTypes.tactic
74 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
77 ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
78 val left : ProofEngineTypes.tactic
80 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
81 Cic.term -> ProofEngineTypes.tactic
83 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
84 val reflexivity : ProofEngineTypes.tactic
86 pattern:ProofEngineTypes.lazy_pattern ->
87 with_what:Cic.lazy_term -> ProofEngineTypes.tactic
89 direction:[ `LeftToRight | `RightToLeft ] ->
90 pattern:ProofEngineTypes.lazy_pattern ->
91 Cic.term -> string list -> ProofEngineTypes.tactic
93 direction:[ `LeftToRight | `RightToLeft ] ->
94 pattern:ProofEngineTypes.lazy_pattern ->
95 Cic.term -> string list -> ProofEngineTypes.tactic
96 val right : ProofEngineTypes.tactic
97 val ring : ProofEngineTypes.tactic
98 val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
100 params:Auto.auto_params ->
101 universe:Universe.universe -> unit -> ProofEngineTypes.tactic
102 val split : ProofEngineTypes.tactic
103 val symmetry : ProofEngineTypes.tactic
104 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
106 Cic.lazy_term option ->
107 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
108 val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
111 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
112 int -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic