From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 27 Nov 2008 09:37:43 +0000 (+0000)
Subject: disambiguation should not fail if the new refiner fails
X-Git-Tag: make_still_working~4497
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bd05377dd2aa36fbbb7edd34726918dab8dd9792;p=helm.git

disambiguation should not fail if the new refiner fails
---

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, _) =