]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/termEditor.ml
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / termEditor.ml
index 4cca702219db51e0a4e9abdba72cb1cd5a4c348b..1b9986caa294184335c6bb697be47b35a6e0a26a 100644 (file)
@@ -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