snapshot, notably:

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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index bb7f2807dee162fe600850abe176d99dd214a773..5b95f4192854fd05fc8efe6f814d87b714925a06 100644 (file)
--- 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)