X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=5b95f4192854fd05fc8efe6f814d87b714925a06;hb=f38e8fafcf040258b54b4032562753a876a8a94e;hp=bb7f2807dee162fe600850abe176d99dd214a773;hpb=142d3076f2a4dc17d9045c2bba4d4b01eddfd008;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index bb7f2807d..5b95f4192 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -72,12 +72,20 @@ class disambiguator
         | Some env -> (false, env)
         | None -> (true, _env)
       in
-      match disambiguate_term ~dbd context metasenv termAst ~aliases:env with
-      | [ (env, metasenv, term) as x ] ->
+      match disambiguate_term ~initial_ugraph:CicUniv.empty_ugraph 
+	~dbd context metasenv termAst ~aliases:env with
+      | [ (env, metasenv, term,ugraph) as x ] ->
           if save_state then self#setEnv env;
           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)