disambiguation should not fail if the new refiner fails

[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 2fbf5a5a1a38f88e3b622ba107dc94f317585d86..2b66594c9477003c292980e5e175c804775d06d4 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -521,7 +521,8 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
            NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty)
        with NGrafiteDisambiguator.DisambiguationError _ ->
         prerr_endline "ERRORE NUOVA DISAMBIGUAZIONE";
-        assert false)
+(*         assert false *)
+       | exn -> ())
     | _ -> ()
   );
   let (diff, metasenv, _, cic, _) =