clean_and_fill optimization

[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..c499d29d277c0f4a9928bcc58f31daa8a20ed86a 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -31,6 +31,9 @@ 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 =
@@ -2146,9 +2149,12 @@ 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 = CicUnivUtils.clean_and_fill uri obj ugraph in
+ let ugraph = clean_and_fill uri obj ugraph in
   CicEnvironment.add_type_checked_obj uri (obj,ugraph)
 
 (** wrappers which instantiate fresh loggers *)
@@ -2160,3 +2166,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
+