Stricter type: the type now shows that disambiguation only alter the lexicon.

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index a0558d9f65a06af2f3703d3826f5f4a678339092..6b5dfca61b829235b852cdc4e7f0a44cd6d52501 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -633,6 +633,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
   in
+(*
  let _try_new cic =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
@@ -721,6 +722,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        )
   )
  in 
+*)
 
 
  try