removed unif_ty ref

[helm.git] / components / cic_unification / cicUnification.ml

diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml
index d1e010ca696558aefe36f8b2ec95f334634aea16..683b3f9df8cdae48a073e85d3e61a69ef81b8386 100644 (file)
--- a/components/cic_unification/cicUnification.ml
+++ b/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 =