*** empty log message ***

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index b0bc8c623aaf5d1bdbc739b2f2090b9ca46af179..b450d25021d35ab496f4bc87a7831c343d833411 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 = HExtlib.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.HExtlib.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 = HExtlib.profile "CicRefine"
+
+let type_of_aux' metasenv context term ugraph =
+ profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
+
+let typecheck metasenv uri obj =
+ profiler2.HExtlib.profile (typecheck metasenv uri) obj