Keeping track of locations of disambiguated ids and symbols.

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

diff --git a/matitaB/matita/matitaScript.ml b/matitaB/matita/matitaScript.ml
index 8d1645858f3c5cc5a36c320d0c779848d7b22ac2..af3cdf12eb15c7a1381e3e3af84f295838974b20 100644 (file)
--- a/matitaB/matita/matitaScript.ml
+++ b/matitaB/matita/matitaScript.ml
@@ -119,7 +119,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
              "Many goals focused. Using the context of the first one\n";
            let _, ctx, _ = NCicUtils.lookup_meta g menv in
             ctx in
-      let newast, m, s, status, t = 
+      let m, s, status, t = 
         GrafiteDisambiguate.disambiguate_nterm 
           status None ctx menv subst (parsed_text,parsed_text_length,
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))