- added Tactics module as a common point where tactics could be accessed

[helm.git] / helm / ocaml / tactics / primitiveTactics.mli

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 5bbc7d188412702d49a8e1a615f30a04c7170664..6538946375ed953be4f0c468bef6fa99d1237be4 100644 (file)
--- 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: