...

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 2b66594c9477003c292980e5e175c804775d06d4..24fdadd5e5e1ad0773ae388240618a1a0258012e 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -507,6 +507,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
+(*
   (match obj with
       CicNotationPt.Theorem (_,_,ty,_) ->
        (try
@@ -521,10 +522,11 @@ 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, _) =
     singleton "third"
       (GrafiteDisambiguator.disambiguate_obj ~lookup_in_library