From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 27 Nov 2008 10:32:18 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4495
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=649a897eeea9908ff6a438dcf6a6969894f9bd7f;p=helm.git

...
---

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 2b66594c9..24fdadd5e 100644
--- 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