From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 16 May 2006 08:23:42 +0000 (+0000)
Subject: more profiling and less assertions
X-Git-Tag: make_still_working~7365
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da971c367f15b855e7a4af88829f1daaadc3bd3c;p=helm.git

more profiling and less assertions
---

diff --git a/helm/software/components/cic_acic/doubleTypeInference.ml b/helm/software/components/cic_acic/doubleTypeInference.ml
index fd9627046..1ea800a6b 100644
--- a/helm/software/components/cic_acic/doubleTypeInference.ml
+++ b/helm/software/components/cic_acic/doubleTypeInference.ml
@@ -303,6 +303,18 @@ let type_of_mutual_inductive_constr uri i j =
 
 let pack_coercion = ref (fun _ _ _ -> assert false);;
 
+let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
+
+let cic_CicHash_add a b c =  
+  profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
+;;
+
+let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
+
+let cic_CicHash_mem a b =  
+  profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
+;;
+
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
  (* Coscoy's double type-inference algorithm             *)
@@ -617,8 +629,8 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
           {synthesized = synthesized' ; expected = Some expectedty'},
           expectedty'
      in
-      assert (not (Cic.CicHash.mem subterms_to_types t));
-      Cic.CicHash.add subterms_to_types t types ;
+(*      assert (not (cic_CicHash_mem subterms_to_types t));*)
+      cic_CicHash_add subterms_to_types t types ;
       res
 
  and visit_exp_named_subst context uri exp_named_subst =