More profiling code.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index b0bc8c623aaf5d1bdbc739b2f2090b9ca46af179..0b63f6a8ce8df63a90f3c6729e285208142c1c23 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -40,9 +40,13 @@ exception AssertFailure of string;;
 
 let debug_print = fun _ -> ()
 
+let profiler = CicUtil.profile "CicRefine.fo_unif"
+
 let fo_unif_subst subst context metasenv t1 t2 ugraph =
   try
+let foo () =
     CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph
+in profiler.CicUtil.profile foo ()
   with
       (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
@@ -1083,3 +1087,11 @@ let type_of_aux' metasenv context term =
      debug_print (lazy ("@@@ REFINE UNCERTAIN: " ^ msg));
      raise e
 ;; *)
+
+let profiler2 = CicUtil.profile "CicRefine"
+
+let type_of_aux' metasenv context term ugraph =
+ profiler2.CicUtil.profile (type_of_aux' metasenv context term) ugraph
+
+let typecheck metasenv uri obj =
+ profiler2.CicUtil.profile (typecheck metasenv uri) obj