X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermEditor.ml;h=1b9986caa294184335c6bb697be47b35a6e0a26a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=4cca702219db51e0a4e9abdba72cb1cd5a4c348b;hpb=cf8abaf99bf9065c82d8f668d441bc4c0a2a13df;p=helm.git

diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml
index 4cca70221..1b9986caa 100644
--- a/helm/gTopLevel/termEditor.ml
+++ b/helm/gTopLevel/termEditor.ml
@@ -101,9 +101,9 @@ module Make(C:DisambiguateTypes.Callbacks) =
        in
         let environment',metasenv,expr,ugraph =
          match
-          Disambiguate'.disambiguate_term ~dbd context metasenv
+          Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
            (input#buffer#get_text ()) ~initial_ugraph:CicUniv.empty_ugraph
-	    !environment
+	    ~aliases:!environment
          with
             [environment',metasenv,expr,u] -> environment',metasenv,expr,u
           | _ -> assert false