X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=b9b4fa42b837d1c64041ad874570add883f40a8d;hb=ffdd3ddd6ce10a5fa0729ab407647bd46c44b9d8;hp=f426f712686e3babe0ef42e0d6d5b92da95eee88;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index f426f7126..b9b4fa42b 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -36,8 +36,8 @@ let refine_term
     let localise t = 
       try NCicUntrusted.NCicHash.find localization_tbl t
       with Not_found -> 
-        prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
-        assert false
+        prerr_endline ("NOT LOCALISED" ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+        (*assert false*) HExtlib.dummy_floc
     in
     let metasenv, subst, term, _ = 
       NCicRefiner.typeof
@@ -61,8 +61,8 @@ let refine_term
 ;;
 
 let refine_obj 
-  ~coercion_db metasenv subst context uri 
-  ~use_coercions obj _ ugraph ~localization_tbl 
+  ~coercion_db metasenv subst context _uri 
+  ~use_coercions obj _ _ugraph ~localization_tbl 
 =
   assert (metasenv=[]);
   assert (subst=[]);
@@ -322,8 +322,7 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.Implicit -> NCic.Implicit `Term
-    | CicNotationPt.UserInput -> assert false (*NCic.Implicit (Some `Hole)
-patterns not implemented *)
+    | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
     | CicNotationPt.Meta (index, subst) ->
@@ -386,6 +385,15 @@ let interpretate_term_option
     ~context 
 ;;
 
+let disambiguate_path path =
+  let localization_tbl = NCicUntrusted.NCicHash.create 23 in
+  fst
+    (interpretate_term_and_interpretate_term_option 
+    ~obj_context:[] ~mk_choice:(fun _ -> assert false)
+    ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
+    ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
+;;
+
 let new_flavour_of_flavour = function 
   | `Definition -> `Definition
   | `MutualDefinition -> `Definition