X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.mli;h=6538946375ed953be4f0c468bef6fa99d1237be4;hb=03cb4be465e546a00f870213b14dcf1b71c4831d;hp=5bbc7d188412702d49a8e1a615f30a04c7170664;hpb=59a077151336a0e73804572b52fb757a0e7f6a97;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 5bbc7d188..653894637 100644
--- a/helm/ocaml/tactics/primitiveTactics.mli
+++ b/helm/ocaml/tactics/primitiveTactics.mli
@@ -37,10 +37,12 @@ val intros_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit ->
    ProofEngineTypes.tactic
 val cut_tac:
-  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term ->
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  term:Cic.term ->
    ProofEngineTypes.tactic 
 val letin_tac:
-  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term ->
+  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  term:Cic.term ->
    ProofEngineTypes.tactic 
 
 val elim_intros_simpl_tac: