X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermEditor.ml;h=f74e45077827dd176d9e676decf506346a317e15;hb=81a63235c649302a1a4691ba37e30282c9c0ef5a;hp=3a74ef05111ce88f2948052896e5ce47a9fc598e;hpb=29442b4d21cf07992ad4e5c981085dada1f90fe4;p=helm.git

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
index 3a74ef051..f74e45077 100644
--- a/helm/gTopLevel/termEditor.ml
+++ b/helm/gTopLevel/termEditor.ml
@@ -56,7 +56,7 @@ module Make(C:DisambiguateTypes.Callbacks) =
 
    module Disambiguate' = DisambiguatingParser.Make(C);;
 
-   class term_editor_impl mqi_handle ?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 mqi_handle context metasenv
+          Disambiguate'.disambiguate_term ~dbd context metasenv
            (input#buffer#get_text ()) !environment
          with
             [environment',metasenv,expr] -> environment',metasenv,expr