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 c499d29d277c0f4a9928bcc58f31daa8a20ed86a..ee76389069b7456a89904c81e1728430476d7d91 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -31,9 +31,6 @@ open Printf
 exception AssertFailure of string;;
 exception TypeCheckerFailure of string;;
 
-let profiler_clean_fill = 
-  (CicUtil.profile "add_obj.typecheck_obj.clean_and_fill").CicUtil.profile
-
 let fdebug = ref 0;;
 let debug t context =
  let rec debug_aux t i =
@@ -2149,13 +2146,10 @@ let typecheck uri =
              uobj,ugraph
 ;;
 
-let clean_and_fill u o g = 
-  (profiler_clean_fill (CicUnivUtils.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 = CicUnivUtils.clean_and_fill uri obj ugraph in
+  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
 
 (** wrappers which instantiate fresh loggers *)