X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftactics.mli;h=780961d6b9645ae6114377c87c54839610403d0a;hb=9415c1b38c7927adab499ddd75f9a19d650a9acd;hp=6bf03b6750ffe94aa2846685dda753af19048eff;hpb=e5efa2e0b70723b431cdc4cffe10b41167145ca4;p=helm.git

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 6bf03b675..780961d6b 100644
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -2,7 +2,7 @@
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
-val auto : ?num:int option -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val auto : ?num:int option -> Mysql.dbd -> ProofEngineTypes.tactic
 val auto_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic
 val change : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic
 val compare : term:Cic.term -> ProofEngineTypes.tactic
@@ -10,7 +10,7 @@ val constructor : n:int -> ProofEngineTypes.tactic
 val contradiction : ProofEngineTypes.tactic
 val cut :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  term:Cic.term -> ProofEngineTypes.tactic
+  Cic.term -> ProofEngineTypes.tactic
 val decide_equality : ProofEngineTypes.tactic
 val decompose :
   ?uris_choice_callback:((UriManager.uri * int *
@@ -36,12 +36,13 @@ val generalize :
 val set_goal : int -> ProofEngineTypes.tactic
 val injection : term:Cic.term -> ProofEngineTypes.tactic
 val intros :
+  ?howmany:int ->
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   unit -> ProofEngineTypes.tactic
 val left : ProofEngineTypes.tactic
 val letin :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  term:Cic.term -> ProofEngineTypes.tactic
+  Cic.term -> ProofEngineTypes.tactic
 val reduce :
   also_in_hypotheses:bool ->
   terms:Cic.term list option -> ProofEngineTypes.tactic
@@ -62,3 +63,6 @@ val transitivity : term:Cic.term -> ProofEngineTypes.tactic
 val whd :
   also_in_hypotheses:bool ->
   terms:Cic.term list option -> ProofEngineTypes.tactic
+val normalize :
+  also_in_hypotheses:bool ->
+  terms:Cic.term list option -> ProofEngineTypes.tactic