]> matita.cs.unibo.it Git - helm.git/commitdiff
Profiling code removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Sep 2005 13:57:25 +0000 (13:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Sep 2005 13:57:25 +0000 (13:57 +0000)
helm/ocaml/cic_proof_checking/cicTypeChecker.ml

index e10a5a6cf29f10c5b75f4001c6215fe2ec31b3ea..ee76389069b7456a89904c81e1728430476d7d91 100644 (file)
@@ -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 *)