X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=b66e12d5e4c15909c2a7badc1d454666168086d2;hb=9d27c7d2161dae5283a9121c206b9184e100c2b5;hp=6dbd312481a0c50e52ef7173787895a0a60bfb14;hpb=6849a0b7b65075049427c27f60d19210ddb52cf5;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 6dbd31248..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"
@@ -909,7 +900,9 @@ struct
   let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
     ?(aliases = DisambiguateTypes.Environment.empty) term
   =
-    let ast = CicNotationParser.parse_level2_ast (Stream.of_string term) in
+    let ast =
+      CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
+    in
     try
       fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
         ?initial_ugraph ~aliases ~universe:None)