]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/texTermEditor.ml
ocaml 3.09 transition
[helm.git] / helm / gTopLevel / texTermEditor.ml
index a59fb3489b2ca0679cac61073c2b6723cfbd0902..5ea965f2fd76c01ffd0c3e23f3210afe8aa38acb 100644 (file)
@@ -221,8 +221,8 @@ module Make(C:DisambiguateTypes.Callbacks) =
         let environment',metasenv,expr,ugraph =
          match
           Disambiguate'.disambiguate_term ~dbd
-           context metasenv (Mathml_editor.get_tex tex_editor) 
-           ~initial_ugraph:CicUniv.empty_ugraph !environment
+           ~context ~metasenv (Mathml_editor.get_tex tex_editor) 
+           ~initial_ugraph:CicUniv.empty_ugraph ~aliases:!environment
          with
             [environment',metasenv,expr,u] -> environment',metasenv,expr,u
           | _ -> assert false