]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tactics/tactics.mli
More daemons/axioms closed.
[helm.git] / components / tactics / tactics.mli
index e9c265c8e3e451a3b45bccc699dc2c3ad97e77d9..fb62b85fc32f680371dec8b1df5d03d6894c8ccf 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 13 14:11:00 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jul  6 11:03:35 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :
@@ -16,6 +16,7 @@ val cases_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   Cic.term -> ProofEngineTypes.tactic
 val change :
+  ?with_cast:bool ->
   pattern:ProofEngineTypes.lazy_pattern ->
   Cic.lazy_term -> ProofEngineTypes.tactic
 val clear : hyps:string list -> ProofEngineTypes.tactic