X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=5ea965f2fd76c01ffd0c3e23f3210afe8aa38acb;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a59fb3489b2ca0679cac61073c2b6723cfbd0902;hpb=cf8abaf99bf9065c82d8f668d441bc4c0a2a13df;p=helm.git diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index a59fb3489..5ea965f2f 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -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