sync with universes and ~subst (and not ?(subst=[]))

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index e9657d191155a8ebb7eddee59dea065ef7e79b1c..cd9d34f0852e5fe9d9f3f327b5597199eb1da307 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -74,13 +74,13 @@ class type disambiguator =
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
       (** @param env @see disambiguateTerm above *)
     method disambiguateTermAst:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) 
   end
 
 (*