commeted out some debugging instructions

[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 f5daaf3d7a9816b2a2eca842072b4214b5737ada..387c747f6d8c064c3fea82a90802e76946a13e03 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -25,6 +25,7 @@
 
 open Printf
 
+(*  (* PROFILING *)
 let apply_subst_counter = ref 0
 let apply_subst_context_counter = ref 0
 let apply_subst_metasenv_counter = ref 0
@@ -34,7 +35,6 @@ let whd_counter = ref 0
 let are_convertible_counter = ref 0
 let metasenv_length = ref 0
 let context_length = ref 0
-
 let reset_counters () =
  apply_subst_counter := 0;
  apply_subst_context_counter := 0;
@@ -45,7 +45,6 @@ let reset_counters () =
  are_convertible_counter := 0;
  metasenv_length := 0;
  context_length := 0
-
 let print_counters () =
   prerr_endline (Printf.sprintf
 "apply_subst: %d
@@ -65,6 +64,7 @@ context length: %d (avg = %.2f)
   !context_length
   ((float !context_length) /. (float !apply_subst_context_counter))
   )
+*)
 
 exception MetaSubstFailure of string
 exception Uncertain of string
@@ -179,13 +179,15 @@ let apply_subst =
      end
   in
   fun s t ->
-    incr apply_subst_counter;
+(*     incr apply_subst_counter; *)
     apply_subst_gen ~appl_fun s t
 ;;
 
 let rec apply_subst_context subst context =
+(*
   incr apply_subst_context_counter;
   context_length := !context_length + List.length context;
+*)
   List.fold_right
     (fun item context ->
       match item with
@@ -204,8 +206,10 @@ let rec apply_subst_context subst context =
     context []
 
 let apply_subst_metasenv subst metasenv =
+(*
   incr apply_subst_metasenv_counter;
   metasenv_length := !metasenv_length + List.length metasenv;
+*)
   List.map
     (fun (n, context, ty) ->
       (n, apply_subst_context subst context, apply_subst subst ty))
@@ -263,7 +267,7 @@ let ppmetasenv ?(sep = "\n") metasenv subst =
  * the calculus *)
 
 let lift subst n term =
-  incr subst_counter;
+(*   incr subst_counter; *)
   let term = apply_subst subst term in
   try
     CicSubstitution.lift n term
@@ -271,7 +275,7 @@ let lift subst n term =
     raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
 
 let subst subst t1 t2 =
-  incr subst_counter;
+(*   incr subst_counter; *)
   let t1 = apply_subst subst t1 in
   let t2 = apply_subst subst t2 in
   try
@@ -280,7 +284,7 @@ let subst subst t1 t2 =
     raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
 
 let whd subst context term =
-  incr whd_counter;
+(*   incr whd_counter; *)
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
   try
@@ -290,7 +294,7 @@ let whd subst context term =
       Printexc.to_string e))
 
 let are_convertible subst context t1 t2 =
-  incr are_convertible_counter;
+(*   incr are_convertible_counter; *)
   let context = apply_subst_context subst context in
   let t1 = apply_subst subst t1 in
   let t2 = apply_subst subst t2 in