X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicUnification.ml;h=683b3f9df8cdae48a073e85d3e61a69ef81b8386;hb=bc2834b671b7e7554159a284f13e52d93debfd03;hp=d1e010ca696558aefe36f8b2ec95f334634aea16;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_unification/cicUnification.ml b/helm/software/components/cic_unification/cicUnification.ml
index d1e010ca6..683b3f9df 100644
--- a/helm/software/components/cic_unification/cicUnification.ml
+++ b/helm/software/components/cic_unification/cicUnification.ml
@@ -39,10 +39,13 @@ let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
 
+let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
+
 let type_of_aux' metasenv subst context term ugraph =
 let foo () =
   try 
-    CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph 
+    profile.HExtlib.profile
+      (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph 
   with
       CicTypeChecker.TypeCheckerFailure msg ->
         let msg =
@@ -389,7 +392,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^
              (lower m1 m2) (upper m1 m2) ugraph
          in
          begin
-         let subst,metasenv,ugraph1 =
+         let subst,metasenv,ugraph1 = 
            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
            (try
               let tyt,ugraph1 =