- new implementation of the apply case in fo_unif using beta expansion

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 512c65d986fa2c48015309faca2a908c7501a654..d5262f44ba8520739a54d16de52890a2df6304c1 100644 (file)
--- 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 ****)