matitaprover is now flexible enough to allow the computation of statistics on

[helm.git] / helm / software / components / binaries / saturate / saturate_main.ml

diff --git a/helm/software/components/binaries/saturate/saturate_main.ml b/helm/software/components/binaries/saturate/saturate_main.ml
index efcfca4eda2a34e3df9815c69ca9da68c35e5641..abb23a67a40df608b0e2526bcab790e08a0a6098 100644 (file)
--- 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 -> 
@@ -64,7 +64,7 @@ struct
       CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
     in
     try
-      fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+      fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ("",0,ast)
         ?initial_ugraph ~aliases ~universe:None)
     with Exit -> raise (Ambiguous_term (lazy term))
 end
@@ -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")