From 26040e5256de231dd309d1b2ab9b12bc36e98368 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 28 Nov 2008 17:48:52 +0000 Subject: [PATCH] it works! --- .../software/components/grafite_parser/grafiteDisambiguate.ml | 4 ++-- helm/software/components/ng_refiner/nCicRefiner.ml | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index e53272387..a6c9effd7 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -78,7 +78,7 @@ let ncic_codomain_of_uri uri = fun _ _ _ -> term) ;; -let ncic_num_choices _ = assert false;; +let ncic_num_choices _ = (*assert false*) [];; let ncic_mk_choice = DisambiguateChoices.mk_choice @@ -554,7 +554,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) = ~context:[] ~metasenv:[] ~subst:[] ~aliases:DisambiguateTypes.Environment.empty ~universe:(Some DisambiguateTypes.Environment.empty) - ("",0,ty) + (text,prefix_len,ty) with | [_,metasenv,subst,ty],_ -> prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!! " ^ diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 8c6c94cb5..479f95802 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -307,7 +307,9 @@ let rec typeof metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev), NCicReduction.head_beta_reduce (C.Appl (outtype::arguments@[term])) - | C.Match _ -> assert false + | C.Match _ as orig -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context orig); + assert false in pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ NCicPp.ppterm ~metasenv ~subst ~context infty )); -- 2.39.2