]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/cicRefine.ml
*** empty log message ***
[helm.git] / helm / ocaml / cic_unification / cicRefine.ml
index 0b63f6a8ce8df63a90f3c6729e285208142c1c23..b450d25021d35ab496f4bc87a7831c343d833411 100644 (file)
@@ -40,13 +40,13 @@ exception AssertFailure of string;;
 
 let debug_print = fun _ -> ()
 
-let profiler = CicUtil.profile "CicRefine.fo_unif"
+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.CicUtil.profile foo ()
+in profiler.HExtlib.profile foo ()
   with
       (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg))
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
@@ -1088,10 +1088,10 @@ let type_of_aux' metasenv context term =
      raise e
 ;; *)
 
-let profiler2 = CicUtil.profile "CicRefine"
+let profiler2 = HExtlib.profile "CicRefine"
 
 let type_of_aux' metasenv context term ugraph =
- profiler2.CicUtil.profile (type_of_aux' metasenv context term) ugraph
+ profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
 
 let typecheck metasenv uri obj =
- profiler2.CicUtil.profile (typecheck metasenv uri) obj
+ profiler2.HExtlib.profile (typecheck metasenv uri) obj