From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 10 Jul 2009 10:03:44 +0000 (+0000)
Subject: more profilers
X-Git-Tag: make_still_working~3703
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b68e52f889215ce2c21c3d771f59b2d2057d53c1;hp=2ecac72aa0961834dd63f0245d2ec563ea96bef2;p=helm.git

more profilers
---

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f86d4d36e..f69de41f5 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -128,6 +128,7 @@ module Superposition (B : Orderings.Blob) =
     let prof_demod_u = HExtlib.profile ~enable "demod.unify";;
     let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";;
     let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";;
+    let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";;
 
     let demod table varlist subterm =
       let cands = 
@@ -145,8 +146,14 @@ module Superposition (B : Orderings.Blob) =
                    prof_demod_u.HExtlib.profile 
                      (Unif.unification (varlist@vl) varlist subterm) side 
                  in 
-                 let side = Subst.apply_subst subst side in
-                 let newside = Subst.apply_subst subst newside in
+                 let side = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) side 
+                 in
+                 let newside = 
+                   prof_demod_s.HExtlib.profile 
+                     (Subst.apply_subst subst) newside 
+                 in
                  if o = Terms.Incomparable then
                    let o = 
                      prof_demod_o.HExtlib.profile