X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=d5262f44ba8520739a54d16de52890a2df6304c1;hb=9945374a5594c068883fa6c775f17b640fcac64d;hp=512c65d986fa2c48015309faca2a908c7501a654;hpb=fb0f22004d533abca8d157ed89665dbf1041e0e2;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 512c65d98..d5262f44b 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -25,6 +25,7 @@
 
 open Printf
 
+
 exception MetaSubstFailure of string
 exception Uncertain of string
 exception AssertFailure of string
@@ -239,6 +240,7 @@ let are_convertible subst context t1 t2 =
   CicReduction.are_convertible context t1 t2
 
 let tempi_type_of_aux_subst = ref 0.0;;
+let tempi_subst = ref 0.0;;
 let tempi_type_of_aux = ref 0.0;;
 
 let type_of_aux' metasenv subst context term =
@@ -261,7 +263,8 @@ let res =
 in
 let time3 = Unix.gettimeofday () in
  tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; 
- tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; 
+ tempi_subst := !tempi_subst +. time2 -. time1 ; 
+ tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ; 
  res
 
 (**** DELIFT ****)