commeted out some debugging instructions

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

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 46a50a63a522eed8c96860e33c8ab4e970c8d912..14d6da3f6de183460f47bc909d223f0cdb917817 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -86,7 +86,9 @@ val fppsubst: Format.formatter -> substitution -> unit
 val fppterm: Format.formatter -> Cic.term -> unit
 val fppmetasenv: Format.formatter -> Cic.metasenv -> unit
 
+(*
 (* DEBUG *)
 val print_counters: unit -> unit
 val reset_counters: unit -> unit
+*)