]> matita.cs.unibo.it Git - helm.git/blobdiff - components/binaries/saturate/saturate_main.ml
rc-1
[helm.git] / components / binaries / saturate / saturate_main.ml
index afe8fbb83f4feffa6b13f87d02ad0a5497465ae6..abb23a67a40df608b0e2526bcab790e08a0a6098 100644 (file)
@@ -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")