X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=c34a5731505c0b9b38d10b11ad91ab1ca9387ce7;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hp=b34a2ec8b91a65e33d35f868bd22f1be9dbac6d1;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
index b34a2ec8b..c34a57315 100644
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
@@ -18,7 +18,7 @@ open DisambiguateTypes
 module Ast = NotationPt
 module NRef = NReference 
 
-let debug_print s = prerr_endline (Lazy.force s);;
+(*let debug_print s = prerr_endline (Lazy.force s);;*)
 let debug_print _ = ();;
 
 let cic_name_of_name = function
@@ -104,9 +104,11 @@ let find_in_context name context =
   aux 1 context
 
 let interpretate_term_and_interpretate_term_option (status: #NCic.status)
-  ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+  ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~universe ~uri ~is_path
   ~localization_tbl 
 =
+  let _ = (mk_choice : GrafiteAst.alias_spec -> NCic.term
+  DisambiguateTypes.codomain_item) in
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
   assert (uri = None);
 
@@ -123,11 +125,22 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
         (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)->
         aux ~localize loc context 
           (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args)))
-    | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) ->
+    | NotationPt.Appl (NotationPt.Symbol (symb, None) :: args) 
+    | NotationPt.Appl
+      (NotationPt.AttributedTerm (_,NotationPt.Symbol (symb,None))::args) ->
         NCic.Implicit `Term
-    | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) ->
+    | NotationPt.Appl (NotationPt.Symbol (symb, Some(uri,desc)) :: args) 
+    | NotationPt.Appl (NotationPt.AttributedTerm 
+      (_,NotationPt.Symbol (symb,Some (uri,desc)))::args) ->
         let cic_args = List.map (aux ~localize loc context) args in
-        Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)
+        (try
+        prerr_endline ("interpr Appl/Sym: " ^ symb);
+        let interpr = Some (GrafiteAst.Symbol_alias (symb, uri, desc)) in
+        Disambiguate.resolve ~mk_choice ~env ~universe (loc (*, Symbol symb*))
+          interpr (`Args cic_args)
+        with Failure err -> 
+          prerr_endline ("resolve of " ^ symb ^ " failed: " ^ err); 
+          assert false)
     | NotationPt.Appl terms ->
        NCic.Appl (List.map (aux ~localize loc context) terms)
     | NotationPt.Binder (binder_kind, (var, typ), body) ->
@@ -182,11 +195,14 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
               raise (Disambiguate.Try_again 
                 (lazy "The type of the term to be matched is still unknown"))
           | None ->
-              let rec fst_constructor =
+              let rec fst_constructor concrete_pat_found =
                 function
-                   (Ast.Pattern (head, href, _), _) :: _ -> 
-                     head, HExtlib.map_option NReference.string_of_reference href
-                 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
+                 | (Ast.Pattern (_, None,_),_)::tl -> fst_constructor true tl
+                 | (Ast.Pattern (head, Some href, _), _) :: _ -> 
+                     head, href 
+                 | (Ast.Wildcard, _) :: tl -> fst_constructor concrete_pat_found tl
+                 | [] when concrete_pat_found -> raise (Disambiguate.Try_again 
+                   (lazy "The type of the term to be matched is still unknown"))
                  | [] -> raise (Invalid_choice (lazy (loc,"The type "^
                      "of the term to be matched cannot be determined "^
                      "because it is an inductive type without constructors "^
@@ -199,19 +215,10 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                         (DisambiguateTypes.string_of_domain_item k ^ " => " ^
                         description_of_alias v)) env; 
 *)
-              (match Disambiguate.resolve ~env ~mk_choice
-                (Id (fst_constructor branches)) (`Args []) with
-              | NCic.Const (NReference.Ref (_,NReference.Con _) as r) -> 
-                   let b,_,_,_,_= NCicEnvironment.get_checked_indtys status r in
-                   NReference.mk_indty b r
-              | NCic.Implicit _ ->
-                 raise (Disambiguate.Try_again 
-                  (lazy "The type of the term to be matched is still unknown"))
-              | t ->
-                raise (DisambiguateTypes.Invalid_choice 
-                  (lazy (loc, 
-                  "The type of the term to be matched is not (co)inductive: " 
-                  ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] t))))
+              let kname,href = fst_constructor false branches in
+              let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status href
+              in
+              NReference.mk_indty b href
          in
          let _,leftsno,itl,_,indtyp_no =
           NCicEnvironment.get_checked_indtys status indtype_ref in
@@ -224,7 +231,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                NCic.Prod (_, _, t) -> 1 + (count_prod t)
              | _ -> 0 
          in 
-         let rec sort branches cl =
+         let rec sort cno branches cl =
           match cl with
              [] ->
               let rec analyze unused unrecognized useless =
@@ -259,6 +266,34 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                      (lazy (loc, "Missing case: " ^ name)))
                 | ((Ast.Wildcard, _) as branch :: _) as branches ->
                     branch, branches
+                | (Ast.Pattern (name',Some href,_),_) as branch :: tl ->
+                  prerr_endline 
+                   (Printf.sprintf "analysis of %s and %s" name name');
+                  (match href with
+                   | NReference.Ref (curi, (NReference.Con (n,cno',_))) ->
+                     (* check che la curi corrisponda alla uri del tipo induttivo *)
+                      let this_indty = NReference.mk_indty true href in
+                      if indtype_ref <> this_indty then
+                        (prerr_endline "fail1";
+                        raise (DisambiguateTypes.Invalid_choice
+                          (lazy (loc, Printf.sprintf 
+                            "Malformed pattern matching: the matching type is %s, but constructor %s belongs to type %s."
+                            (NReference.string_of_reference indtype_ref)
+                            (NReference.string_of_reference href)
+                            (NReference.string_of_reference this_indty)))))
+                      else
+                              if cno = cno' then (prerr_endline "ok";branch, tl)
+                        else
+                              (prerr_endline (Printf.sprintf "skip %d %d" cno cno');
+                              let found,rest = find_and_remove tl in
+                          found, branch::rest)
+                   | _ ->
+                     (prerr_endline "fail2";
+                     raise
+                      (DisambiguateTypes.Invalid_choice
+                       (lazy (loc,"Malformed pattern: found " ^ 
+                                  (NReference.string_of_reference href) ^
+                                  " which is not a type constructor.")))))
                 | (Ast.Pattern (name',_,_),_) as branch :: tl
                    when name = name' ->
                     branch,tl
@@ -270,7 +305,7 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                match branch with
                   Ast.Pattern (name,y,args),term ->
                    if List.length args = count_prod ty - leftsno then
-                    ((name,y,args),term)::sort tl cltl
+                    ((name,y,args),term)::sort (cno+1) tl cltl
                    else
                     raise
                      (DisambiguateTypes.Invalid_choice
@@ -285,9 +320,9 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
                            mk_lambdas (n - 1))
                    in
                     (("wildcard",None,[]),
-                     mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+                     mk_lambdas (count_prod ty - leftsno)) :: sort (cno+1) tl cltl
          in
-          let branches = sort branches cl in
+          let branches = sort 1 branches cl in
            NCic.Match (indtype_ref, cic_outtype, cic_term,
             (List.map do_branch branches))
     | NotationPt.Cast (t1, t2) ->
@@ -327,9 +362,10 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
     | NotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | NotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
     | NotationPt.UserInput -> NCic.Implicit `Hole
-    | NotationPt.Num (num, None) -> NCic.Implicit `Closed
-    | NotationPt.Num (num, i) -> 
-        Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
+    | NotationPt.Num (num, i) ->
+        let i = HExtlib.map_option 
+          (fun (uri,desc) -> GrafiteAst.Number_alias (uri,desc)) i in
+        Disambiguate.resolve ~env ~universe ~mk_choice (loc(*,Num*)) i (`Num_arg num)
     | NotationPt.Meta (index, subst) ->
         let cic_subst =
          List.map
@@ -345,8 +381,12 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
     | NotationPt.Sort (`NCProp s) -> NCic.Sort (NCic.Type
        [`CProp,NUri.uri_of_string ("cic:/matita/pts/Type" ^ s ^ ".univ")])
     | NotationPt.Symbol (symbol, instance) ->
-        Disambiguate.resolve ~env ~mk_choice 
-         (Symbol (symbol, instance)) (`Args [])
+        let instance = HExtlib.map_option 
+           (fun (uri,desc) -> GrafiteAst.Symbol_alias (symbol, uri, desc))
+           instance
+        in
+        Disambiguate.resolve ~env ~universe ~mk_choice 
+         (loc (*,Symbol symbol*)) instance (`Args [])
     | NotationPt.Variable _
     | NotationPt.Magic _
     | NotationPt.Layout _
@@ -368,24 +408,24 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status)
    (fun ~context -> aux_option ~localize:true HExtlib.dummy_floc context)
 ;;
 
-let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~uri
+let interpretate_term status ?(create_dummy_ids=false) ~context ~env ~universe ~uri
  ~is_path ast ~obj_context ~localization_tbl ~mk_choice
 =
   let context = List.map fst context in
   fst 
     (interpretate_term_and_interpretate_term_option status
-      ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+      ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
       ~localization_tbl)
     ~context ast
 ;;
 
-let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env ~uri
- ~is_path ~localization_tbl ~mk_choice ~obj_context
+let interpretate_term_option status ?(create_dummy_ids=false) ~context ~env
+  ~universe ~uri ~is_path ~localization_tbl ~mk_choice ~obj_context
 =
   let context = List.map fst context in
   snd 
     (interpretate_term_and_interpretate_term_option status
-      ~obj_context ~mk_choice ~create_dummy_ids ~env ~uri ~is_path
+      ~obj_context ~mk_choice ~create_dummy_ids ~env ~universe ~uri ~is_path
       ~localization_tbl)
     ~context 
 ;;
@@ -395,7 +435,8 @@ let disambiguate_path status path =
   fst
     (interpretate_term_and_interpretate_term_option status
     ~obj_context:[] ~mk_choice:(fun _ -> assert false)
-    ~create_dummy_ids:true ~env:DisambiguateTypes.Environment.empty
+    ~create_dummy_ids:true ~env:DisambiguateTypes.InterprEnv.empty
+    ~universe:DisambiguateTypes.Environment.empty
     ~uri:None ~is_path:true ~localization_tbl) ~context:[] path
 ;;
 
@@ -406,7 +447,7 @@ let ncic_name_of_ident = function
 
 let interpretate_obj status
 (*      ?(create_dummy_ids=false)  *)
-     ~context ~env ~uri ~is_path obj ~localization_tbl ~mk_choice 
+     ~context ~env ~universe ~uri ~is_path obj ~localization_tbl ~mk_choice 
 =
  assert (context = []);
  assert (is_path = false);
@@ -419,7 +460,7 @@ let interpretate_obj status
  | NotationPt.Theorem (flavour, name, ty, bo, pragma) ->
      let ty' = 
        interpretate_term status
-         ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false ty 
+         ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false ty 
      in
      let height = (* XXX calculate *) 0 in
      uri, height, [], [], 
@@ -454,13 +495,13 @@ let interpretate_obj status
                    in
                    let cic_body =
                      interpretate_term status
-                       ~obj_context ~context ~env ~uri:None ~is_path:false
+                       ~obj_context ~context ~env ~universe ~uri:None ~is_path:false
                        (add_binders `Lambda body) 
                    in
                    let cic_type =
                      interpretate_term_option status
                        ~obj_context:[]
-                       ~context ~env ~uri:None ~is_path:false `Type
+                       ~context ~env ~universe ~uri:None ~is_path:false `Type
                        (HExtlib.map_option (add_binders `Pi) typ)
                    in
                    ([],ncic_name_of_ident name, decr_idx, cic_type, cic_body))
@@ -471,7 +512,7 @@ let interpretate_obj status
          | bo -> 
              let bo = 
                interpretate_term status
-                ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
+                ~obj_context:[] ~context:[] ~env ~universe ~uri:None ~is_path:false bo
              in
              let attrs = `Provided, flavour, pragma in
              NCic.Constant ([],name,Some bo,ty',attrs)))
@@ -486,7 +527,7 @@ let interpretate_obj status
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
-          interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+          interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
            ~is_path:false t
          in
           (name,NCic.Decl t)::context,(name,t)::res
@@ -511,14 +552,14 @@ let interpretate_obj status
       (fun (name,_,ty,cl) ->
         let ty' =
          add_params
-         (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+         (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
            ~is_path:false ty) in
         let cl' =
          List.map
           (fun (name,ty) ->
             let ty' =
              add_params
-              (interpretate_term status ~obj_context ~context ~env ~uri:None
+              (interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
                 ~is_path:false ty) in
             let relevance = [] in
              relevance,name,ty'
@@ -542,7 +583,7 @@ let interpretate_obj status
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
-          interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+          interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
            ~is_path:false t
          in
           (name,NCic.Decl t)::context,(name,t)::res
@@ -554,7 +595,7 @@ let interpretate_obj status
     let leftno = List.length params in
     let ty' =
      add_params
-      (interpretate_term status ~obj_context:[] ~context ~env ~uri:None
+      (interpretate_term status ~obj_context:[] ~context ~env ~universe ~uri:None
         ~is_path:false ty) in
     let nref =
      NReference.reference_of_spec uri (NReference.Ind (true,0,leftno)) in
@@ -564,7 +605,7 @@ let interpretate_obj status
       List.fold_left
        (fun (context,res) (name,ty,_coercion,_arity) ->
          let ty =
-          interpretate_term status ~obj_context ~context ~env ~uri:None
+          interpretate_term status ~obj_context ~context ~env ~universe ~uri:None
            ~is_path:false ty in
          let context' = (name,NCic.Decl ty)::context in
           context',(name,ty)::res
@@ -595,6 +636,29 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names
     | Ast.Num(m,_), GrafiteAst.Number_alias (uri,desc) -> Ast.Num(m,Some (uri,desc))
     | _ -> assert false
   in
+  let lookup_choices =
+     fun item ->
+      (*match universe with
+      | None -> 
+          lookup_in_library 
+            interactive_user_uri_choice 
+            input_or_locate_uri item
+      | Some e ->
+          (try Environment.find item e
+          with Not_found -> [])
+*)
+          (try 
+             let res = Environment.find item universe in
+             let id = match item with
+               | DisambiguateTypes.Id id -> id
+               | DisambiguateTypes.Symbol _ -> "SYM"
+               | DisambiguateTypes.Num _ -> "NUM"
+             in
+             debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id
+               (List.length res)));
+             res
+          with Not_found -> [])
+   in
   let init = initialize_ast ~universe ~lookup_in_library in
   let init_var ~local_names (n,ty) = 
           (n,HExtlib.map_option (init ~local_names) ty)
@@ -613,40 +677,25 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names
   let init_pattern ~local_names = function
     | Ast.Wildcard as t -> local_names,t
     | Ast.Pattern (c,uri,vars) -> 
-        (* XXX verificare ordine *)
         let ln',vars' = init_vars ~local_names vars in
-        ln',Ast.Pattern (c,uri,vars')
+        let uri' = match uri with
+          | Some _ -> uri
+          | None -> 
+             let choices = lookup_choices (DisambiguateTypes.Id c) in
+             if List.length choices <> 1 then None
+             else (match (List.hd choices) with
+             | GrafiteAst.Ident_alias (_,u) -> 
+                 Some (NReference.reference_of_string u)
+             | _ -> assert false)
+        in
+        ln',Ast.Pattern (c,uri',vars')
   in
   let mk_alias = function
-    | Ast.Ident (id,_) -> DisambiguateTypes.Id (id,None)
-    | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol (sym,None)
-    | Ast.Num _ -> DisambiguateTypes.Num None
+    | Ast.Ident (id,_) -> DisambiguateTypes.Id id
+    | Ast.Symbol (sym,_) -> DisambiguateTypes.Symbol sym
+    | Ast.Num _ -> DisambiguateTypes.Num
     | _ -> assert false
   in
-  let lookup_choices =
-     fun item ->
-      (*match universe with
-      | None -> 
-          lookup_in_library 
-            interactive_user_uri_choice 
-            input_or_locate_uri item
-      | Some e ->
-          (try Environment.find item e
-          with Not_found -> [])
-*)
-          (try 
-             let res = Environment.find item universe in
-             let id = match item with
-               | DisambiguateTypes.Id (id,None) -> id ^ "?"
-               | DisambiguateTypes.Id (id,_) -> id ^ "!"
-               | DisambiguateTypes.Symbol _ -> "SYM"
-               | DisambiguateTypes.Num _ -> "NUM"
-             in
-             prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
-               (List.length res));
-             res
-          with Not_found -> [])
-   in
    match t with
    | Ast.Ident (id,(`Ambiguous|`Rel))
        when List.mem id local_names -> Ast.Ident (id,`Rel)
@@ -671,7 +720,19 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names
          List.map (fun (p,u) ->
            let ns,p' = init_pattern ~local_names p in
            p',init ~local_names:ns u) pl in
-       Ast.Case (t',ity,oty',pl')
+       let ity' = HExtlib.map_option 
+         (fun (ity_id,href) -> 
+            let href' = match href with
+            | None -> 
+               let choices = lookup_choices (DisambiguateTypes.Id ity_id) in
+               if List.length choices <> 1 then None
+               else (match (List.hd choices) with
+                 | GrafiteAst.Ident_alias (_,u) ->
+                    Some (NReference.reference_of_string u)
+                 | _ -> assert false)
+            | Some _ -> href
+            in (ity_id,href')) ity
+       in Ast.Case (t',ity',oty',pl')
    | Ast.Cast (u,v) -> Ast.Cast (init ~local_names u,init ~local_names v)
    | Ast.LetIn ((n,ty),u,v) -> 
        let n' = cic_name_of_name n in
@@ -694,7 +755,7 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names
    | t -> t
 ;;
 
-let initialize_obj ~universe ~lookup_in_library o = 
+let initialize_obj ~universe ~lookup_in_library o =
   let init = initialize_ast ~universe ~lookup_in_library in
   let init_var ~local_names (n,ty) = 
           (n,HExtlib.map_option (init ~local_names) ty)
@@ -726,65 +787,62 @@ let initialize_obj ~universe ~lookup_in_library o =
       in
       Ast.Inductive (ls',itl')
   | Ast.Theorem (flav,n,ty,bo,p) ->
-      Ast.Theorem (flav,n,init ~local_names:[] ty,
-                   HExtlib.map_option (init ~local_names:[]) bo,p)
+      let ty' = init ~local_names:[] ty in
+      let bo' = HExtlib.map_option (init ~local_names:[]) bo in 
+      Ast.Theorem (flav,n,ty',bo',p)
   | Ast.Record (ls,n,ty,fl) ->
       let ln,ls' = init_vars ~local_names:[] ls in
       let ty' = init ~local_names:ln ty in
-      let fl' = List.map (fun (fn,fty,b,i) -> 
-              fn,init ~local_names:ln fty,b,i) fl in
-      Ast.Record (ls,n,ty',fl')
+      let _,fl' = List.fold_left (fun (ln0,fl0) (fn,fty,b,i) -> 
+        (fn::ln0,(fn,init ~local_names:ln0 fty,b,i)::fl0)) (ln,[]) fl 
+      in
+      let fl' = List.rev fl' in
+      Ast.Record (ls',n,ty',fl')
 ;;
 
 let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
  ~expty ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
  ~aliases ~universe ~lookup_in_library (text,prefix_len,term) 
 =
+  let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
   let local_names = List.map (fun (n,_) -> n) context in
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
-   let res,b =
-    MultiPassDisambiguator.disambiguate_thing
-     ~freshen_thing:NotationUtil.freshen_term
-     ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias ~fix_instance
+    Disambiguate.disambiguate_thing
+     ~context ~metasenv ~subst ~use_coercions:true 
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
-     ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
-     ~passes:(MultiPassDisambiguator.passes ())
-     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
+     ~initial_ugraph:() ~expty
+     ~mk_implicit ~description_of_alias ~fix_instance ~aliases 
+     ~universe ~lookup_in_library 
+     ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
+     ~domain_of_thing:Disambiguate.domain_of_term
      ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
      ~refine_thing:(refine_term status) 
      (text,prefix_len,
       (initialize_ast ~universe ~lookup_in_library ~local_names term))
      ~visit:Disambiguate.bfvisit
-     ~mk_localization_tbl ~expty ~subst
-   in
-    List.map (function (a,b,c,d,_) -> term,a,b,c,d) res, b
+     ~mk_localization_tbl
 ;;
 
-
 let disambiguate_obj (status: #NCicCoercion.status)
    ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
-   let res,b =
-    MultiPassDisambiguator.disambiguate_thing
-     ~freshen_thing:NotationUtil.freshen_obj
-     ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias ~fix_instance
+  let obj' = initialize_obj ~universe ~lookup_in_library obj in
+    Disambiguate.disambiguate_thing
+     ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true 
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
-     ~universe 
-     ~uri:(Some uri)
-     ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
-     ~passes:(MultiPassDisambiguator.passes ())
-     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+     ~initial_ugraph:() ~expty:None
+     ~mk_implicit ~description_of_alias ~fix_instance ~aliases 
+     ~universe ~lookup_in_library 
+     ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+     ~pp_term:(NotationPp.pp_term status)
+     ~domain_of_thing:Disambiguate.domain_of_obj
      ~interpretate_thing:(interpretate_obj status ~mk_choice)
      ~refine_thing:(refine_obj status) 
-     (text,prefix_len,(initialize_obj ~universe ~lookup_in_library obj))
+     (text,prefix_len,obj')
      ~visit:Disambiguate.bfvisit_obj
-     ~mk_localization_tbl ~expty:None
-   in
-    List.map (function (a,b,c,d,_) -> a,b,c,d) res, b
+     ~mk_localization_tbl
 ;;
 (*
 let _ =