the filled object is inserted in the env after a successful typechecking

[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 ee76389069b7456a89904c81e1728430476d7d91..18de8af5e22047e54a668519cf997aa556f7c34b 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -2148,7 +2148,7 @@ let typecheck uri =
 
 let typecheck_obj ~logger uri obj =
  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph, univlist = CicUnivUtils.clean_and_fill uri obj ugraph in
+ let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
   CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
 
 (** wrappers which instantiate fresh loggers *)