- ng_refiner:

[helm.git] / matita / matita / matitaScript.ml

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 74a95bb107d00fa6972c04187932fff3b7c0c49b..d86871963437efbac813b5e63b590f98573af5ff 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -121,7 +121,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
             ctx in
       let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
-          status None ctx menv subst (parsed_text,parsed_text_length,
+          status `XTNone ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in