permutation.ma added to the repository.

[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 c16385e5d4597c5785ec2fd298f11f872972345e..ee76389069b7456a89904c81e1728430476d7d91 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -2148,8 +2148,8 @@ let typecheck uri =
 
 let typecheck_obj ~logger uri obj =
  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
-  CicEnvironment.add_type_checked_obj uri (obj,ugraph)
+ let ugraph, univlist = CicUnivUtils.clean_and_fill uri obj ugraph in
+  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
 
 (** wrappers which instantiate fresh loggers *)
 
@@ -2160,3 +2160,4 @@ let type_of_aux' ?(subst = []) metasenv context t ugraph =
 let typecheck_obj uri obj =
  let logger = new CicLogger.logger in
  typecheck_obj ~logger uri obj
+