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

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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index bb7f2807dee162fe600850abe176d99dd214a773..46341acfdf03c3ea401bc7910424ec24f4c81211 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -72,8 +72,9 @@ 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