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

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
index 3a74ef051..e7b50c266 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 ~(dbh:Dbi.connection) ?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 ~dbh context metasenv
            (input#buffer#get_text ()) !environment
          with
             [environment',metasenv,expr] -> environment',metasenv,expr