1 (* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jun 1 13:27:04 CEST 2007 *)
2 val absurd : term:Cic.term -> ProofEngineTypes.tactic
3 val apply : term:Cic.term -> ProofEngineTypes.tactic
7 params:(string * string) list ->
8 universe:Universe.universe -> ProofEngineTypes.tactic
9 val assumption : ProofEngineTypes.tactic
12 params:(string * string) list ->
13 universe:Universe.universe -> ProofEngineTypes.tactic
16 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
17 Cic.term -> ProofEngineTypes.tactic
19 pattern:ProofEngineTypes.lazy_pattern ->
20 Cic.lazy_term -> ProofEngineTypes.tactic
21 val clear : hyps:string list -> ProofEngineTypes.tactic
22 val clearbody : hyp:string -> ProofEngineTypes.tactic
23 val constructor : n:int -> ProofEngineTypes.tactic
24 val contradiction : ProofEngineTypes.tactic
26 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
27 Cic.term -> ProofEngineTypes.tactic
30 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
31 unit -> ProofEngineTypes.tactic
33 dbd:HSql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
34 val destruct : term:Cic.term -> ProofEngineTypes.tactic
36 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
39 ?pattern:ProofEngineTypes.lazy_pattern ->
40 Cic.term -> ProofEngineTypes.tactic
41 val elim_intros_simpl :
42 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
45 ?pattern:ProofEngineTypes.lazy_pattern ->
46 Cic.term -> ProofEngineTypes.tactic
48 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
49 ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
50 val exact : term:Cic.term -> ProofEngineTypes.tactic
51 val exists : ProofEngineTypes.tactic
52 val fail : Tacticals.tactic
54 reduction:ProofEngineTypes.lazy_reduction ->
56 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
57 val fourier : ProofEngineTypes.tactic
59 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
60 dbd:HSql.dbd -> string -> ProofEngineTypes.tactic
62 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
63 ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
64 val id : Tacticals.tactic
67 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
68 unit -> ProofEngineTypes.tactic
69 val inversion : term:Cic.term -> ProofEngineTypes.tactic
71 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
74 ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
75 val left : ProofEngineTypes.tactic
77 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
78 Cic.term -> ProofEngineTypes.tactic
80 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
81 val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
82 val reflexivity : ProofEngineTypes.tactic
84 pattern:ProofEngineTypes.lazy_pattern ->
85 with_what:Cic.lazy_term -> ProofEngineTypes.tactic
87 direction:[ `LeftToRight | `RightToLeft ] ->
88 pattern:ProofEngineTypes.lazy_pattern ->
89 Cic.term -> string list -> ProofEngineTypes.tactic
91 direction:[ `LeftToRight | `RightToLeft ] ->
92 pattern:ProofEngineTypes.lazy_pattern ->
93 Cic.term -> string list -> ProofEngineTypes.tactic
94 val right : ProofEngineTypes.tactic
95 val ring : ProofEngineTypes.tactic
96 val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
97 val split : ProofEngineTypes.tactic
98 val subst : ProofEngineTypes.tactic
99 val symmetry : ProofEngineTypes.tactic
100 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
102 Cic.lazy_term option ->
103 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
104 val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
107 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
108 Cic.term -> Cic.term -> ProofEngineTypes.tactic