]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/termEditor.ml
no longer use Dbi module but directly use Mysql module since it's 13
[helm.git] / helm / gTopLevel / termEditor.ml
index e7b50c2662efadad81dcfb91615bc6cb505d200b..f74e45077827dd176d9e676decf506346a317e15 100644 (file)
@@ -56,7 +56,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
 
    module Disambiguate' = DisambiguatingParser.Make(C);;
 
-   class term_editor_impl ~(dbh:Dbi.connection) ?packing ?width ?height
+   class term_editor_impl ~(dbd:Mysql.dbd) ?packing ?width ?height
     ?isnotempty_callback ?share_environment_with () : term_editor
    =
     let environment =
@@ -100,7 +100,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
        in
         let environment',metasenv,expr =
          match
-          Disambiguate'.disambiguate_term ~dbh context metasenv
+          Disambiguate'.disambiguate_term ~dbd context metasenv
            (input#buffer#get_text ()) !environment
          with
             [environment',metasenv,expr] -> environment',metasenv,expr