From bd05377dd2aa36fbbb7edd34726918dab8dd9792 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 27 Nov 2008 09:37:43 +0000
Subject: [PATCH] disambiguation should not fail if the new refiner fails

---
 helm/software/components/grafite_parser/grafiteDisambiguate.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 2fbf5a5a1..2b66594c9 100644
--- 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, _) =
-- 
2.39.2