From 649a897eeea9908ff6a438dcf6a6969894f9bd7f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Nov 2008 10:32:18 +0000 Subject: [PATCH] ... --- .../software/components/grafite_parser/grafiteDisambiguate.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- 2.39.2