it works!

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index e53272387620c3feeef887bef59485108863dcd6..a6c9effd7e02fd1cdd3c363abe4f6a8baca6b6de 100644 (file)
--- 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 8c6c94cb576f30c1397aacecfe4966ab9f0c49b8..479f95802059ce9db3a81034a4aac5e61681010f 100644 (file)
--- 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 ));