added universes list handling

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index c499d29d277c0f4a9928bcc58f31daa8a20ed86a..e10a5a6cf29f10c5b75f4001c6215fe2ec31b3ea 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -2154,8 +2154,8 @@ let clean_and_fill u o g =
 
 let typecheck_obj ~logger uri obj =
  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph = clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_obj uri (obj,ugraph)
+ let ugraph, univlist = clean_and_fill uri obj ugraph in
+  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
 
 (** wrappers which instantiate fresh loggers *)