X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=6b5dfca61b829235b852cdc4e7f0a44cd6d52501;hb=a7237500e8a2a4237a6ae8ba4b8301f7bbcb6acb;hp=a0558d9f65a06af2f3703d3826f5f4a678339092;hpb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index a0558d9f6..6b5dfca61 100644 --- 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