X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_unification%2FcicMetaSubst.ml;h=3536623287f02712a2bb21655ad02137e69b1398;hb=df8f668d1369432dbfb7c74a4c4789f3353fcb45;hp=5870089beda2d9f208f318cbd22789d87a60c73f;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml
index 5870089be..353662328 100644
--- a/components/cic_unification/cicMetaSubst.ml
+++ b/components/cic_unification/cicMetaSubst.ml
@@ -1,4 +1,5 @@
 (* Copyright (C) 2003, HELM Team.
+ * 
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -230,7 +231,7 @@ let apply_subst_gen ~appl_fun subst term =
        in
        C.CoFix (i, fl')
  in
-  LibrarySync.merge_coercions (um_aux term)
+  um_aux term
 ;;
 
 let apply_subst =
@@ -252,6 +253,11 @@ let apply_subst =
     apply_subst_gen ~appl_fun s t
 ;;
 
+let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
+let apply_subst s t = 
+  profiler.HExtlib.profile (apply_subst s) t
+
+
 let rec apply_subst_context subst context =
 (*
   incr apply_subst_context_counter;