1 (* GENERATED FILE, DO NOT EDIT. STAMP:Mon Apr 16 17:26:20 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
11 params:(string * string) list ->
12 dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
14 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
15 Cic.term -> ProofEngineTypes.tactic
17 pattern:ProofEngineTypes.lazy_pattern ->
18 Cic.lazy_term -> ProofEngineTypes.tactic
19 val clear : hyps:string list -> ProofEngineTypes.tactic
20 val clearbody : hyp:string -> ProofEngineTypes.tactic
21 val constructor : n:int -> ProofEngineTypes.tactic
22 val contradiction : ProofEngineTypes.tactic
24 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
25 Cic.term -> ProofEngineTypes.tactic
28 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
29 unit -> ProofEngineTypes.tactic
31 dbd:HMysql.dbd -> universe:Universe.universe -> ProofEngineTypes.tactic
32 val destruct : term:Cic.term -> ProofEngineTypes.tactic
34 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
37 ?pattern:ProofEngineTypes.lazy_pattern ->
38 Cic.term -> ProofEngineTypes.tactic
39 val elim_intros_simpl :
40 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
43 ?pattern:ProofEngineTypes.lazy_pattern ->
44 Cic.term -> ProofEngineTypes.tactic
46 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
47 ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
48 val exact : term:Cic.term -> ProofEngineTypes.tactic
49 val exists : ProofEngineTypes.tactic
50 val fail : ProofEngineTypes.tactic
52 reduction:ProofEngineTypes.lazy_reduction ->
54 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
55 val fourier : ProofEngineTypes.tactic
57 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
58 dbd:HMysql.dbd -> string -> ProofEngineTypes.tactic
60 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
61 ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
62 val id : ProofEngineTypes.tactic
65 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
66 unit -> ProofEngineTypes.tactic
67 val inversion : term:Cic.term -> ProofEngineTypes.tactic
69 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
72 ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
73 val left : ProofEngineTypes.tactic
75 ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
76 Cic.term -> ProofEngineTypes.tactic
78 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
79 val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
80 val reflexivity : ProofEngineTypes.tactic
82 pattern:ProofEngineTypes.lazy_pattern ->
83 with_what:Cic.lazy_term -> ProofEngineTypes.tactic
85 direction:[ `LeftToRight | `RightToLeft ] ->
86 pattern:ProofEngineTypes.lazy_pattern ->
87 Cic.term -> string list -> ProofEngineTypes.tactic
89 direction:[ `LeftToRight | `RightToLeft ] ->
90 pattern:ProofEngineTypes.lazy_pattern ->
91 Cic.term -> string list -> ProofEngineTypes.tactic
92 val right : ProofEngineTypes.tactic
93 val ring : ProofEngineTypes.tactic
94 val set_goal : int -> ProofEngineTypes.tactic
95 val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
96 val split : ProofEngineTypes.tactic
97 val subst : ProofEngineTypes.tactic
98 val symmetry : ProofEngineTypes.tactic
99 val transitivity : term:Cic.term -> ProofEngineTypes.tactic
101 Cic.lazy_term option ->
102 pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
103 val whd : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic