Got rid of a few warnings.

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 6afef50e050f2fb69a5f4e7ad0b9292f7cea9dd1..bf9ade7b113daecd60b171436f045ec0e55b7c4b 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -156,7 +156,7 @@ let rec auto dbd = function
 ;; 
 
 
-let auto_tac  ?num ~(dbd:Mysql.dbd) =
+let auto_tac ?num dbd =
   let auto_tac dbh (proof,goal) =
   debug_print "Entro in Auto";
   match (auto dbd [(proof, [(goal,depth)],None)]) with

diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli
index 0b5a9ca9b35d9dcae5b17d4a651263c09d6742d7..4095457ae591411d6f1b59f5b3b44392fedaf5f9 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.mli
+++ b/helm/ocaml/tactics/autoTactic.mli
@@ -24,5 +24,5 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val auto_tac : ?num:int option -> dbd:Mysql.dbd -> ProofEngineTypes.tactic
+val auto_tac : ?num:int option -> Mysql.dbd -> ProofEngineTypes.tactic
 val auto_tac_new : dbd:Mysql.dbd -> ProofEngineTypes.tactic

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 8abb946c6686e27a64e9060b5089c5c35a69ce23..7bbdbf6b068ece8400f291b3fc459a115076ba8a 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -405,7 +405,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
  in
   mk_tactic (intros_tac ~mk_fresh_name_callback ())
   
-let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let cut_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)
@@ -440,7 +440,7 @@ let cut_tac?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[
  in
   mk_tactic (cut_tac ~mk_fresh_name_callback term)
 
-let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) ~term=
+let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
  let letin_tac
   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
   term (proof, goal)

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 0ab82af2a8d612c3b6db745d63e87a8b1ed0b37a..81385510c15c10a8e11aa1ed6a57f19f6698a3f2 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.mli
+++ b/helm/ocaml/tactics/primitiveTactics.mli
@@ -44,11 +44,11 @@ val intros_tac:
    ProofEngineTypes.tactic
 val cut_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  term:Cic.term ->
+  Cic.term ->
    ProofEngineTypes.tactic 
 val letin_tac:
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  term:Cic.term ->
+  Cic.term ->
    ProofEngineTypes.tactic 
 
 val elim_intros_simpl_tac:

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index a91985290838195bfcd4a9813a0d5de8b5c674a9..780961d6b9645ae6114377c87c54839610403d0a 100644 (file)
--- 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 *
@@ -42,7 +42,7 @@ val intros :
 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