]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/disambiguatingParser.ml.in
no longer use Dbi module but directly use Mysql module since it's 13
[helm.git] / helm / gTopLevel / disambiguatingParser.ml.in
index dfab60433c75d285dd38e1590071d7303fa68dc9..224eb4b6e913bf4bf58cc262838154a381c2e910 100644 (file)
@@ -31,14 +31,14 @@ module AndreaAndZackDisambiguatingParser =
 
   module Make (C : DisambiguateTypes.Callbacks) =
    struct
-    let disambiguate_term ~(dbh:Dbi.connection) context metasenv term_as_string
+    let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term_as_string
       aliases
     =
       let module Disambiguate' = Disambiguate.Make (C) in
       let term =
         CicTextualParser2.parse_term (Stream.of_string term_as_string)
       in
-      Disambiguate'.disambiguate_term ~dbh context metasenv term ~aliases
+      Disambiguate'.disambiguate_term ~dbd context metasenv term ~aliases
    end
  end