From 9d27c7d2161dae5283a9121c206b9184e100c2b5 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 21 Sep 2005 16:48:13 +0000
Subject: [PATCH] This commit removes the slowest identity function ever
implemented!
---
helm/ocaml/cic_disambiguation/disambiguate.ml | 11 +----------
1 file changed, 1 insertion(+), 10 deletions(-)
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 054826cca..b66e12d5e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -691,7 +691,6 @@ module Make (C: Callbacks) =
uris
let refine_profiler = CicUtil.profile "disambiguate_thing.refine_thing"
-let disambiguate_environment_merge_profiler = CicUtil.profile "disambiguate_thing.disambiguate_environment_merge"
let disambiguate_thing ~dbd ~context ~metasenv
?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
@@ -857,15 +856,7 @@ in refine_profiler.CicUtil.profile foo ()
!choices_avg
(float_of_int (!domain_size - 1) *. !choices_avg *. (float_of_int res_size) +. !choices_avg))));
*)
- let choices, b = res in
-let foo () =
- (List.map
- (fun (env, metasenv, t, ugraph) ->
- Environment.fold Environment.add env aliases,
- metasenv, t, ugraph)
- choices),
- b
-in disambiguate_environment_merge_profiler.CicUtil.profile foo ()
+ res
with
CicEnvironment.CircularDependency s ->
failwith "Disambiguate: circular dependency"
--
2.39.2