snapshot, notably:

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

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