X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Fsaturate%2Fsaturate_main.ml;h=abb23a67a40df608b0e2526bcab790e08a0a6098;hb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;hp=afe8fbb83f4feffa6b13f87d02ad0a5497465ae6;hpb=8f9d476c32c48d14348a61889dc191c7696bd404;p=helm.git

diff --git a/helm/software/components/binaries/saturate/saturate_main.ml b/helm/software/components/binaries/saturate/saturate_main.ml
index afe8fbb83..abb23a67a 100644
--- a/helm/software/components/binaries/saturate/saturate_main.ml
+++ b/helm/software/components/binaries/saturate/saturate_main.ml
@@ -32,7 +32,7 @@ sig
     * choice from the user is needed to disambiguate the term
     * @raise Ambiguous_term for ambiguous term *)
   val disambiguate_string:
-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->
     ?context:Cic.context ->
     ?metasenv:Cic.metasenv ->
     ?initial_ugraph:CicUniv.universe_graph -> 
@@ -73,7 +73,7 @@ let configuration_file = ref "../../../matita/matita.conf.xml";;
 
 let core_notation_script = "../../../matita/core_notation.moo";;
 
-let get_from_user ~(dbd:HMysql.dbd) =
+let get_from_user ~(dbd:HSql.dbd) =
   let rec get () =
     match read_line () with
     | "" -> []
@@ -144,7 +144,7 @@ let main () =
   Helm_registry.load_from !configuration_file;
   ignore (CicNotation2.load_notation [] core_notation_script);
   ignore (CicNotation2.load_notation [] "../../../matita/library/legacy/coq.ma");
-  let dbd = HMysql.quick_connect
+  let dbd = HSql.quick_connect
     ~host:(Helm_registry.get "db.host")
     ~user:(Helm_registry.get "db.user")
     ~database:(Helm_registry.get "db.database")