From 9415c1b38c7927adab499ddd75f9a19d650a9acd Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jun 2005 15:39:29 +0000
Subject: [PATCH] Got rid of a few warnings.

---
 helm/ocaml/tactics/autoTactic.ml        | 2 +-
 helm/ocaml/tactics/autoTactic.mli       | 2 +-
 helm/ocaml/tactics/primitiveTactics.ml  | 4 ++--
 helm/ocaml/tactics/primitiveTactics.mli | 4 ++--
 helm/ocaml/tactics/tactics.mli          | 6 +++---
 5 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 6afef50e0..bf9ade7b1 100644
--- 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 0b5a9ca9b..4095457ae 100644
--- 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 8abb946c6..7bbdbf6b0 100644
--- 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 0ab82af2a..81385510c 100644
--- 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 a91985290..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 *
@@ -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
-- 
2.39.2