X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=5b95f4192854fd05fc8efe6f814d87b714925a06;hb=87ff483dd776e580fa97fca0e3bf888cc8a8d540;hp=46341acfdf03c3ea401bc7910424ec24f4c81211;hpb=3bec70852905f57198cd5b659dc72d430c1c5d2c;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 46341acfd..5b95f4192 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -79,6 +79,13 @@ class disambiguator
           x
       | _ -> assert false
 
+    method disambiguateTermAsts ?(metasenv = []) ?env asts =
+      let ast = CicAst.pack asts in
+      let (env, metasenv, term, ugraph) =
+        self#disambiguateTermAst ~context:[] ~metasenv ?env ast
+      in
+      (env, metasenv, CicUtil.unpack term, ugraph)
+
     method disambiguateTerm ?context ?metasenv ?env stream =
       self#disambiguateTermAst ?context ?metasenv ?env
         (parserr#parseTerm stream)