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 ?pattern:ProofEngineTypes.lazy_pattern ->
18 Cic.term -> ProofEngineTypes.tactic
21 pattern:ProofEngineTypes.lazy_pattern ->
22 Cic.lazy_term -> ProofEngineTypes.tactic
23 val clear : hyps:string list -> ProofEngineTypes.tactic
24 val clearbody : hyp:string -> ProofEngineTypes.tactic
25 val constructor : n:int -> ProofEngineTypes.tactic
26 val contradiction : ProofEngineTypes.tactic
28 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
29 Cic.term -> ProofEngineTypes.tactic
32 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
33 unit -> ProofEngineTypes.tactic
36 params:Auto.auto_params ->
37 universe:Universe.universe -> ProofEngineTypes.tactic
38 val destruct : Cic.term list option -> ProofEngineTypes.tactic
40 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
43 ?pattern:ProofEngineTypes.lazy_pattern ->
44 Cic.term -> ProofEngineTypes.tactic
45 val elim_intros_simpl :
46 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
49 ?pattern:ProofEngineTypes.lazy_pattern ->
50 Cic.term -> ProofEngineTypes.tactic
52 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
53 ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
54 val exact : term:Cic.term -> ProofEngineTypes.tactic
55 val exists : ProofEngineTypes.tactic
56 val fail : Tacticals.tactic
58 reduction:ProofEngineTypes.lazy_reduction ->
60 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
61 val fourier : ProofEngineTypes.tactic
63 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
64 dbd:HSql.dbd -> string -> ProofEngineTypes.tactic
66 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
67 ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
68 val id : Tacticals.tactic
71 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
72 unit -> ProofEngineTypes.tactic
73 val inversion : term:Cic.term -> ProofEngineTypes.tactic
75 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
78 ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
79 val left : ProofEngineTypes.tactic
81 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
82 Cic.term -> ProofEngineTypes.tactic
84 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
85 val reflexivity : ProofEngineTypes.tactic
87 pattern:ProofEngineTypes.lazy_pattern ->
88 with_what:Cic.lazy_term -> ProofEngineTypes.tactic
90 direction:[ `LeftToRight | `RightToLeft ] ->
91 pattern:ProofEngineTypes.lazy_pattern ->
92 Cic.term -> string list -> ProofEngineTypes.tactic
94 direction:[ `LeftToRight | `RightToLeft ] ->
95 pattern:ProofEngineTypes.lazy_pattern ->
96 Cic.term -> string list -> ProofEngineTypes.tactic
97 val right : ProofEngineTypes.tactic
98 val ring : ProofEngineTypes.tactic
99 val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
101 params:Auto.auto_params ->
102 universe:Universe.universe -> unit -> ProofEngineTypes.tactic
103 val split : ProofEngineTypes.tactic
104 val symmetry : ProofEngineTypes.tactic
105 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
107 Cic.lazy_term option ->
108 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
109 val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
112 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
113 int -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic