-(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Dec 21 00:41:09 CET 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Dec 29 00:00:27 CET 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val reflexivity : ProofEngineTypes.tactic
+val rename : froms:string list -> tos:string list -> ProofEngineTypes.tactic
val replace :
pattern:ProofEngineTypes.lazy_pattern ->
with_what:Cic.lazy_term -> ProofEngineTypes.tactic
val rewrite :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->
- Cic.term -> ProofEngineTypes.tactic
+ Cic.term -> string list -> ProofEngineTypes.tactic
val rewrite_simpl :
direction:[ `LeftToRight | `RightToLeft ] ->
pattern:ProofEngineTypes.lazy_pattern ->
- Cic.term -> ProofEngineTypes.tactic
+ Cic.term -> string list -> ProofEngineTypes.tactic
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
val set_goal : int -> ProofEngineTypes.tactic