From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Sep 2005 13:57:25 +0000 (+0000)
Subject: Profiling code removed.
X-Git-Tag: LAST_BEFORE_NEW~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=49f2e946e8359d5ee070f4134b7d1afbd9d78219;p=helm.git

Profiling code removed.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index e10a5a6cf..ee7638906 100644
--- 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,12 +2146,9 @@ 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, univlist = clean_and_fill uri obj ugraph in
+ 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 *)