according to camlp5 sources, the dummy loc should be 0,0 and not -1,-1

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 5c198cb5962bf06bef7850892ba384ffe2c35618..9d42899c6895fffeeb3366f210c7dd6a3fbbe2f4 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -35,9 +35,9 @@ module Ast = CicNotationPt
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *

- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *

   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *

-  Token.flocation option * string Lazy.t * bool) list
+  (Stdpp.location * string) Lazy.t * bool) list

 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)


@@ -47,7 +47,7 @@ type aliases = bool * DisambiguateTypes.environment
 type 'a disambiguator_input = string * int * 'a
 
 type domain = domain_tree list
 type 'a disambiguator_input = string * int * 'a
 
 type domain = domain_tree list

-and domain_tree = Node of Token.flocation list * domain_item * domain
+and domain_tree = Node of Stdpp.location list * domain_item * domain

 
 let rec string_of_domain =
  function
 
 let rec string_of_domain =
  function


@@ -86,7 +86,7 @@ let uniq_domain dom =
  in
   snd (aux [] dom)
 
  in
   snd (aux [] dom)
 

-let debug = true
+let debug = false

 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 (*


@@ -103,58 +103,61 @@ let descr_of_domain_item = function
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 
  | Symbol (s, _) -> s
  | Num i -> string_of_int i
 

-type 'a test_result =
-  | Ok of 'a * Cic.metasenv
-  | Ko of Token.flocation option * string Lazy.t
-  | Uncertain of Token.flocation option * string Lazy.t
+type ('term,'metasenv,'subst,'graph) test_result =
+  | Ok of 'term * 'metasenv * 'subst * 'graph
+  | Ko of (Stdpp.location * string) Lazy.t
+  | Uncertain of (Stdpp.location * string) Lazy.t

 
 

-let refine_term metasenv context uri term ugraph ~localization_tbl =
+let refine_term metasenv subst context uri term ugraph ~localization_tbl =

 (*   if benchmark then incr actual_refinements; *)
   assert (uri=None);
     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
     try
       let term', _, metasenv',ugraph1 = 
        CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
 (*   if benchmark then incr actual_refinements; *)
   assert (uri=None);
     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
     try
       let term', _, metasenv',ugraph1 = 
        CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in

-       (Ok (term', metasenv')),ugraph1
+      (Ok (term', metasenv',[],ugraph1))

     with
      exn ->
       let rec process_exn loc =
        function
     with
      exn ->
       let rec process_exn loc =
        function

-          HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+          HExtlib.Localized (loc,exn) -> process_exn loc exn

         | CicRefine.Uncertain msg ->
             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
         | CicRefine.Uncertain msg ->
             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;

-            Uncertain (loc,msg),ugraph
+            Uncertain (lazy (loc,Lazy.force msg))

         | CicRefine.RefineFailure msg ->
             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
               (CicPp.ppterm term) (Lazy.force msg)));
         | CicRefine.RefineFailure msg ->
             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
               (CicPp.ppterm term) (Lazy.force msg)));

-            Ko (loc,msg),ugraph
+            Ko (lazy (loc,Lazy.force msg))

        | exn -> raise exn
       in
        | exn -> raise exn
       in

-       process_exn None exn
+       process_exn Stdpp.dummy_loc exn

 
 

-let refine_obj metasenv context uri obj ugraph ~localization_tbl =
- assert (context = []);
+let refine_obj metasenv subst context uri obj ugraph ~localization_tbl =
+   assert (context = []);
+   assert (metasenv = []);
+   assert (subst = []);

    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
    try
      let obj', metasenv,ugraph =
    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
    try
      let obj', metasenv,ugraph =

-      CicRefine.typecheck metasenv uri obj ~localization_tbl
+       CicRefine.typecheck metasenv uri obj ~localization_tbl

      in
      in

-       (Ok (obj', metasenv)),ugraph
+     (Ok (obj', metasenv,[],ugraph))

    with
      exn ->
       let rec process_exn loc =
        function
    with
      exn ->
       let rec process_exn loc =
        function

-          HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+          HExtlib.Localized (loc,exn) -> process_exn loc exn

         | CicRefine.Uncertain msg ->
         | CicRefine.Uncertain msg ->

-            debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
-            Uncertain (loc,msg),ugraph
+            debug_print (lazy ("UNCERTAIN!!! [" ^ 
+              (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
+            Uncertain (lazy (loc,Lazy.force msg))

         | CicRefine.RefineFailure msg ->
             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
               (CicPp.ppobj obj) (Lazy.force msg))) ;
         | CicRefine.RefineFailure msg ->
             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
               (CicPp.ppobj obj) (Lazy.force msg))) ;

-            Ko (loc,msg),ugraph
+            Ko (lazy (loc,Lazy.force msg))

        | exn -> raise exn
       in
        | exn -> raise exn
       in

-       process_exn None exn
+       process_exn Stdpp.dummy_loc exn

 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try


@@ -172,11 +175,12 @@ let find_in_context name context =
   in
   aux 1 context
 
   in
   aux 1 context
 

-let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast

      ~localization_tbl
 =
      ~localization_tbl
 =

+  (* create_dummy_ids shouldbe used only for interpretating patterns *)

   assert (uri = None);
   assert (uri = None);

-  let rec aux ~localize loc (context: Cic.name list) = function
+  let rec aux ~localize loc context = function

     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
          if localize then Cic.CicHash.add localization_tbl res loc;
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
         let res = aux ~localize loc context term in
          if localize then Cic.CicHash.add localization_tbl res loc;


@@ -202,21 +206,24 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
         let cic_term = aux ~localize loc context term in
         let cic_outtype = aux_option ~localize loc context None outtype in
         let do_branch ((head, _, args), term) =
         let cic_term = aux ~localize loc context term in
         let cic_outtype = aux_option ~localize loc context None outtype in
         let do_branch ((head, _, args), term) =

-          let rec do_branch' context = function
-            | [] -> aux ~localize loc context term
-            | (name, typ) :: tl ->
-                let cic_name = CicNotationUtil.cic_name_of_name name in
-                let cic_body = do_branch' (cic_name :: context) tl in
-                let typ =
-                  match typ with
-                  | None -> Cic.Implicit (Some `Type)
-                  | Some typ -> aux ~localize loc context typ
-                in
-                Cic.Lambda (cic_name, typ, cic_body)
-          in
+         let rec do_branch' context = function
+           | [] -> aux ~localize loc context term
+           | (name, typ) :: tl ->
+               let cic_name = CicNotationUtil.cic_name_of_name name in
+               let cic_body = do_branch' (cic_name :: context) tl in
+               let typ =
+                 match typ with
+                 | None -> Cic.Implicit (Some `Type)
+                 | Some typ -> aux ~localize loc context typ
+               in
+               Cic.Lambda (cic_name, typ, cic_body)
+         in

           do_branch' context args
         in
           do_branch' context args
         in

-        let (indtype_uri, indtype_no) =
+        let indtype_uri, indtype_no =
+          if create_dummy_ids then
+            (UriManager.uri_of_string "cic:/fake_indty.con", 0)
+          else

           match indty_ident with
           | Some (indty_ident, _) ->
              (match resolve env (Id indty_ident) () with
           match indty_ident with
           | Some (indty_ident, _) ->
              (match resolve env (Id indty_ident) () with


@@ -225,21 +232,112 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->

-                raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))

           | None ->
           | None ->

-              let fst_constructor =
-                match branches with
-                | ((head, _, _), _) :: _ -> head
-                | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
+              let rec fst_constructor =
+                function
+                   (Ast.Pattern (head, _, _), _) :: _ -> head
+                 | (Ast.Wildcard, _) :: tl -> fst_constructor tl
+                 | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))

               in
               in

-              (match resolve env (Id fst_constructor) () with
+              (match resolve env (Id (fst_constructor branches)) () with

               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                   (indtype_uri, indtype_no)
               | Cic.Implicit _ ->
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
                   (indtype_uri, indtype_no)
               | Cic.Implicit _ ->
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->

-                raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+        in
+        let branches =
+         if create_dummy_ids then
+          List.map
+           (function
+               Ast.Wildcard,term -> ("wildcard",None,[]), term
+             | Ast.Pattern _,_ ->
+                raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+           ) branches
+         else
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
+            Cic.InductiveDefinition (il,_,leftsno,_) ->
+             let _,_,_,cl =
+              try
+               List.nth il indtype_no
+              with _ -> assert false
+             in
+              let rec count_prod t =
+                match CicReduction.whd [] t with
+                    Cic.Prod (_, _, t) -> 1 + (count_prod t)
+                  | _ -> 0 
+              in 
+              let rec sort branches cl =
+               match cl with
+                  [] ->
+                   let rec analyze unused unrecognized useless =
+                    function
+                       [] ->
+                        if unrecognized != [] then
+                         raise (Invalid_choice
+                          (Some loc,
+                           lazy
+                            ("Unrecognized constructors: " ^
+                             String.concat " " unrecognized)))
+                        else if useless > 0 then
+                         raise (Invalid_choice
+                          (Some loc,
+                           lazy
+                            ("The last " ^ string_of_int useless ^
+                             "case" ^ if useless > 1 then "s are" else " is" ^
+                             " unused")))
+                        else
+                         []
+                     | (Ast.Wildcard,_)::tl when not unused ->
+                         analyze true unrecognized useless tl
+                     | (Ast.Pattern (head,_,_),_)::tl when not unused ->
+                         analyze unused (head::unrecognized) useless tl
+                     | _::tl -> analyze unused unrecognized (useless + 1) tl
+                   in
+                    analyze false [] 0 branches
+                | (name,ty)::cltl ->
+                   let rec find_and_remove =
+                    function
+                       [] ->
+                        raise
+                         (Invalid_choice
+                          (Some loc, lazy ("Missing case: " ^ name)))
+                     | ((Ast.Wildcard, _) as branch :: _) as branches ->
+                         branch, branches
+                     | (Ast.Pattern (name',_,_),_) as branch :: tl
+                        when name = name' ->
+                         branch,tl
+                     | branch::tl ->
+                        let found,rest = find_and_remove tl in
+                         found, branch::rest
+                   in
+                    let branch,tl = find_and_remove branches in
+                    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
+                        else
+                         raise
+                          (Invalid_choice
+                           (Some loc,
+                             lazy ("Wrong number of arguments for " ^ name)))
+                     | Ast.Wildcard,term ->
+                        let rec mk_lambdas =
+                         function
+                            0 -> term
+                          | n ->
+                             CicNotationPt.Binder
+                              (`Lambda, (CicNotationPt.Ident ("_", None), None),
+                                mk_lambdas (n - 1))
+                        in
+                         (("wildcard",None,[]),
+                          mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+              in
+               sort branches cl
+          | _ -> assert false

         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))


@@ -250,13 +348,13 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in

-        let cic_def =
+        let cic_typ =

           match typ with
           match typ with

-          | None -> cic_def
-          | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+          | None -> Cic.Implicit (Some `Type)
+          | Some t -> aux ~localize loc context t

         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in

-        Cic.LetIn (cic_name, cic_def, cic_body)
+        Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)

     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left


@@ -285,6 +383,8 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->

+                     (* since we avoid the letin, the context has no
+                      * recfuns in it *)

                      let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false
                      let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false


@@ -336,9 +436,9 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in

-         let build_term funs (var,_,_,_) t =
+         let build_term funs (var,_,ty,_) t =

           incr counter;
           incr counter;

-          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)

          in
           (match cic_body with
               `AvoidLetInNoAppl n ->
          in
           (match cic_body with
               `AvoidLetInNoAppl n ->


@@ -382,23 +482,23 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->

-                       raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+                       raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))

                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in
           (try 
             match cic with
             | Cic.Const (uri, []) ->
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in
           (try 
             match cic with
             | Cic.Const (uri, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try
                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try

-                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with
                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with


@@ -411,7 +511,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->

-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in

                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->


@@ -426,10 +526,10 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
 *)
                 t
             | _ ->
 *)
                 t
             | _ ->

-              raise (Invalid_choice (lazy "??? Can this happen?"))
+              raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))

            with 
              CicEnvironment.CircularDependency _ -> 
            with 
              CicEnvironment.CircularDependency _ -> 

-               raise (Invalid_choice (lazy "Circular dependency in the environment"))))
+               raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))

     | CicNotationPt.Implicit -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
     | CicNotationPt.Implicit -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()


@@ -445,11 +545,11 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)

-    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)

     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)

-  and aux_option ~localize loc (context: Cic.name list) annotation = function
+  and aux_option ~localize loc context annotation = function

     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
   in


@@ -459,7 +559,8 @@ let interpretate_path ~context path =
  let localization_tbl = Cic.CicHash.create 23 in
   (* here we are throwing away useful localization informations!!! *)
   fst (
  let localization_tbl = Cic.CicHash.create 23 in
   (* here we are throwing away useful localization informations!!! *)
   fst (

-   interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
+   interpretate_term ~create_dummy_ids:true 
+    ~context ~env:Environment.empty ~uri:None ~is_path:true

     path ~localization_tbl, localization_tbl)
 
 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
     path ~localization_tbl, localization_tbl)
 
 let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =


@@ -563,6 +664,16 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
       | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
       | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))

+;;
+
+let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
+     ~localization_tbl
+=
+  let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in
+interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
+~localization_tbl
+;;
+

           
 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.AttributedTerm (`Loc loc, term) ->
           
 let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.AttributedTerm (`Loc loc, term) ->


@@ -629,20 +740,25 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in
   | Ast.Case (term, indty_ident, outtype, branches) ->
       let term_dom = domain_of_term ~loc ~context term in
       let outtype_dom = domain_of_term_option ~loc ~context outtype in

-      let get_first_constructor = function
+      let rec get_first_constructor = function

         | [] -> []
         | [] -> []

-        | ((head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ] in
-      let do_branch ((head, _, args), term) =
-        let (term_context, args_domain) =
-          List.fold_left
-            (fun (cont, dom) (name, typ) ->
-              (CicNotationUtil.cic_name_of_name name :: cont,
-               (match typ with
-               | None -> dom
-               | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
-            (context, []) args
-        in
-        domain_of_term ~loc ~context:term_context term @ args_domain
+        | (Ast.Pattern (head, _, _), _) :: _ -> [ Node ([loc], Id head, []) ]
+        | _ :: tl -> get_first_constructor tl in
+      let do_branch =
+       function
+          Ast.Pattern (head, _, args), term ->
+           let (term_context, args_domain) =
+             List.fold_left
+               (fun (cont, dom) (name, typ) ->
+                 (CicNotationUtil.cic_name_of_name name :: cont,
+                  (match typ with
+                  | None -> dom
+                  | Some typ -> dom @ domain_of_term ~loc ~context:cont typ)))
+               (context, []) args
+           in
+            domain_of_term ~loc ~context:term_context term @ args_domain
+        | Ast.Wildcard, term ->
+            domain_of_term ~loc ~context term

       in
       let branches_dom =
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in
       in
       let branches_dom =
         List.fold_left (fun dom branch -> dom @ do_branch branch) [] branches in


@@ -684,7 +800,8 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))

-            @ domain_of_term_option ~loc ~context typ
+            @ dom
+            @ domain_of_term_option ~loc ~context:context' typ

             @ domain_of_term ~loc ~context:context' body
           ) [] defs
       in
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
       in


@@ -730,6 +847,7 @@ let domain_of_term ~context term =
  uniq_domain (domain_of_term ~context term)
 
 let domain_of_obj ~context ast =
  uniq_domain (domain_of_term ~context term)
 
 let domain_of_obj ~context ast =

+ let context = List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context in

  assert (context = []);
   match ast with
    | Ast.Theorem (_,_,ty,bo) ->
  assert (context = []);
   match ast with
    | Ast.Theorem (_,_,ty,bo) ->


@@ -780,6 +898,14 @@ let domain_of_obj ~context ast =
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 
 let domain_of_obj ~context obj = 
  uniq_domain (domain_of_obj ~context obj)
 

+let domain_of_ast_term = domain_of_term;;
+
+let domain_of_term ~context term = 
+ let context = 
+   List.map (function None -> Cic.Anonymous | Some (n,_) -> n) context 
+ in
+ domain_of_term ~context term
+

   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)
   (* dom1 \ dom2 *)
 let domain_diff dom1 dom2 =
 (* let domain_diff = Domain.diff *)


@@ -807,30 +933,67 @@ let domain_diff dom1 dom2 =
 
 module type Disambiguator =
 sig
 
 module type Disambiguator =
 sig

+  val disambiguate_thing:
+    dbd:HSql.dbd ->
+    context:'context ->
+    metasenv:'metasenv ->
+    subst:'subst ->
+    initial_ugraph:'ugraph ->
+    hint: ('metasenv -> 'raw_thing -> 'raw_thing) * 
+          (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+              ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+    aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+    universe:DisambiguateTypes.codomain_item list
+             DisambiguateTypes.Environment.t option ->
+    uri:'uri ->
+    pp_thing:('ast_thing -> string) ->
+    domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+    interpretate_thing:(context:'context ->
+                        env:DisambiguateTypes.codomain_item
+                            DisambiguateTypes.Environment.t ->
+                        uri:'uri ->
+                        is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
+    refine_thing:('metasenv ->
+                  'subst ->
+                  'context ->
+                  'uri ->
+                  'raw_thing ->
+                  'ugraph -> localization_tbl:'cichash -> 
+                  ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+    localization_tbl:'cichash ->
+    string * int * 'ast_thing ->
+    ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
+     list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
+    list * bool
+

   val disambiguate_term :
     ?fresh_instances:bool ->
   val disambiguate_term :
     ?fresh_instances:bool ->

-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->

     context:Cic.context ->
     context:Cic.context ->

-    metasenv:Cic.metasenv ->
+    metasenv:Cic.metasenv -> 
+    subst:Cic.substitution ->
+    ?goal:int ->

     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     CicNotationPt.term disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     CicNotationPt.term disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)

+     Cic.substitution *

      Cic.term*
      CicUniv.universe_graph) list *  (* disambiguated term *)
     bool
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
      Cic.term*
      CicUniv.universe_graph) list *  (* disambiguated term *)
     bool
 
   val disambiguate_obj :
     ?fresh_instances:bool ->

-    dbd:HMysql.dbd ->
+    dbd:HSql.dbd ->

     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)

+     Cic.substitution *

      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
     bool
      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
     bool


@@ -874,19 +1037,16 @@ module Make (C: Callbacks) =
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
 
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 

-    let disambiguate_thing ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+    let disambiguate_thing ~dbd ~context ~metasenv ~subst
+      ~initial_ugraph:base_univ ~hint
+      ~aliases ~universe

       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 

+      ~localization_tbl

       (thing_txt,thing_txt_prefix_len,thing)
     =
       debug_print (lazy "DISAMBIGUATE INPUT");
       (thing_txt,thing_txt_prefix_len,thing)
     =
       debug_print (lazy "DISAMBIGUATE INPUT");

-      let disambiguate_context =  (* cic context -> disambiguate context *)
-        List.map
-          (function None -> Cic.Anonymous | Some (name, _) -> name)
-          context
-      in

       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));

-      let thing_dom = domain_of_thing ~context:disambiguate_context thing in
+      let thing_dom = domain_of_thing ~context thing in

       debug_print
        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
 (*
       debug_print
        (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
 (*


@@ -972,36 +1132,39 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
               aux (aux env l) tl in
         let filled_env = aux aliases todo_dom in
         try
               aux (aux env l) tl in
         let filled_env = aux aliases todo_dom in
         try

-          let localization_tbl = Cic.CicHash.create 503 in

           let cic_thing =
           let cic_thing =

-            interpretate_thing ~context:disambiguate_context ~env:filled_env
+            interpretate_thing ~context ~env:filled_env

              ~uri ~is_path:false thing ~localization_tbl
           in
              ~uri ~is_path:false thing ~localization_tbl
           in

+          let cic_thing = (fst hint) metasenv cic_thing in

 let foo () =
 let foo () =

-          let k,ugraph1 =
-           refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
+          let k =
+           refine_thing metasenv subst 
+             context uri cic_thing ugraph ~localization_tbl

           in
           in

-            (k , ugraph1 )
+          let k = (snd hint) k in
+            k

 in refine_profiler.HExtlib.profile foo ()
         with
 in refine_profiler.HExtlib.profile foo ()
         with

-        | Try_again msg -> Uncertain (None,msg), ugraph
-        | Invalid_choice msg -> Ko (None,msg), ugraph
+        | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+        | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg))
+        | Invalid_choice (Some loc,msg) -> Ko (lazy (loc,Lazy.force msg))

       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
       (* aux returns triples Ok/Uncertain/Ko *)
       (* rem_dom is the concatenation of all the remainin domains *)
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
       (* aux returns triples Ok/Uncertain/Ko *)
       (* rem_dom is the concatenation of all the remainin domains *)

-      let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom base_univ =
+      let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =

         debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
         match todo_dom with
         | [] ->
             assert (lookup_in_todo_dom = None);
             (match test_env aliases rem_dom base_univ with
         debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
         match todo_dom with
         | [] ->
             assert (lookup_in_todo_dom = None);
             (match test_env aliases rem_dom base_univ with

-            | Ok (thing, metasenv),new_univ -> 
-               [ aliases, diff, metasenv, thing, new_univ ], [], []
-            | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true]
-            | Uncertain (loc,msg),new_univ ->
-               [],[aliases,diff,loc,msg,new_univ],[])
+            | Ok (thing, metasenv,subst,new_univ) -> 
+               [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
+            | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
+            | Uncertain loc_msg ->
+               [],[aliases,diff,loc_msg],[])

         | Node (locs,item,inner_dom) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
         | Node (locs,item,inner_dom) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));


@@ -1012,8 +1175,9 @@ in refine_profiler.HExtlib.profile foo ()
             match choices with
                [] ->
                 [], [],
             match choices with
                [] ->
                 [], [],

-                 [aliases, diff, Some (List.hd locs),
-                  lazy ("No choices for " ^ string_of_domain_item item),
+                 [aliases, diff, 
+                  (lazy (List.hd locs,
+                    "No choices for " ^ string_of_domain_item item)),

                   true]
 (*
              | [codomain_item] ->
                   true]
 (*
              | [codomain_item] ->


@@ -1053,81 +1217,82 @@ in refine_profiler.HExtlib.profile foo ()
              | _::_ ->
                  let mark_not_significant failures =
                    List.map
              | _::_ ->
                  let mark_not_significant failures =
                    List.map

-                    (fun (env, diff, loc, msg, _b) ->
-                      env, diff, loc, msg, false)
+                    (fun (env, diff, loc_msg, _b) ->
+                      env, diff, loc_msg, false)

                     failures in
                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
                   if ok_l <> [] || uncertain_l <> [] then
                    ok_l,uncertain_l,mark_not_significant error_l
                   else
                    outcome in
                     failures in
                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
                   if ok_l <> [] || uncertain_l <> [] then
                    ok_l,uncertain_l,mark_not_significant error_l
                   else
                    outcome in

-               let rec filter univ = function 
+               let rec filter = function 

                 | [] -> [],[],[]
                 | codomain_item :: tl ->
                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
                     let new_env = Environment.add item codomain_item aliases in
                     let new_diff = (item,codomain_item)::diff in
                     (match
                 | [] -> [],[],[]
                 | codomain_item :: tl ->
                     debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
                     let new_env = Environment.add item codomain_item aliases in
                     let new_diff = (item,codomain_item)::diff in
                     (match

-                      test_env new_env (inner_dom@remaining_dom@rem_dom) univ
+                      test_env new_env 
+                        (inner_dom@remaining_dom@rem_dom) base_univ

                      with
                      with

-                    | Ok (thing, metasenv),new_univ ->
+                    | Ok (thing, metasenv,subst,new_univ) ->

                         let res = 
                           (match inner_dom with
                           | [] ->
                         let res = 
                           (match inner_dom with
                           | [] ->

-                             [new_env,new_diff,metasenv,thing,new_univ], [], []
+                             [new_env,new_diff,metasenv,subst,thing,new_univ],
+                             [], []

                           | _ ->
                              aux new_env new_diff None inner_dom
                           | _ ->
                              aux new_env new_diff None inner_dom

-                              (remaining_dom@rem_dom) new_univ
+                              (remaining_dom@rem_dom) 

                           ) 
                         in
                           ) 
                         in

-                         res @@ filter univ tl
-                    | Uncertain (loc,msg),new_univ ->
+                         res @@ filter tl
+                    | Uncertain loc_msg ->

                         let res =
                           (match inner_dom with
                         let res =
                           (match inner_dom with

-                          | [] -> [],[new_env,new_diff,loc,msg,new_univ],[]
+                          | [] -> [],[new_env,new_diff,loc_msg],[]

                           | _ ->
                              aux new_env new_diff None inner_dom
                           | _ ->
                              aux new_env new_diff None inner_dom

-                              (remaining_dom@rem_dom) new_univ
+                              (remaining_dom@rem_dom) 

                           )
                         in
                           )
                         in

-                         res @@ filter univ tl
-                    | Ko (loc,msg),_ ->
-                        let res = [],[],[new_env,new_diff,loc,msg,true] in
-                         res @@ filter univ tl)
+                         res @@ filter tl
+                    | Ko loc_msg ->
+                        let res = [],[],[new_env,new_diff,loc_msg,true] in
+                         res @@ filter tl)

                in
                 let ok_l,uncertain_l,error_l =
                in
                 let ok_l,uncertain_l,error_l =

-                 classify_errors (filter base_univ choices)
+                 classify_errors (filter choices)

                 in
                  let res_after_ok_l =
                   List.fold_right
                 in
                  let res_after_ok_l =
                   List.fold_right

-                   (fun (env,diff,_,_,univ) res ->
-                     aux env diff None remaining_dom rem_dom univ @@ res
+                   (fun (env,diff,_,_,_,_) res ->
+                     aux env diff None remaining_dom rem_dom @@ res

                    ) ok_l ([],[],error_l)
                 in
                  List.fold_right
                    ) ok_l ([],[],error_l)
                 in
                  List.fold_right

-                  (fun (env,diff,_,_,univ) res ->
-                    aux env diff None remaining_dom rem_dom univ @@ res
+                  (fun (env,diff,_) res ->
+                    aux env diff None remaining_dom rem_dom @@ res

                   ) uncertain_l res_after_ok_l
       in
                   ) uncertain_l res_after_ok_l
       in

-      let aux' aliases diff lookup_in_todo_dom todo_dom base_univ =
+      let aux' aliases diff lookup_in_todo_dom todo_dom =

        match test_env aliases todo_dom base_univ with
        match test_env aliases todo_dom base_univ with

-        | Ok _,_
-        | Uncertain _,_ ->
-           aux aliases diff lookup_in_todo_dom todo_dom [] base_univ
-        | Ko (loc,msg),_ -> [],[],[aliases,diff,loc,msg,true] in
-      let base_univ = initial_ugraph in
+        | Ok _
+        | Uncertain _ ->
+           aux aliases diff lookup_in_todo_dom todo_dom [] 
+        | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in

       try
         let res =
       try
         let res =

-         match aux' aliases [] None todo_dom base_univ with
+         match aux' aliases [] None todo_dom with

          | [],uncertain,errors ->
             let errors =
              List.map
          | [],uncertain,errors ->
             let errors =
              List.map

-              (fun (env,diff,loc,msg,_) -> (env,diff,loc,msg,true)
+              (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)

               ) uncertain @ errors
             in
             let errors =
              List.map
               ) uncertain @ errors
             in
             let errors =
              List.map

-              (fun (env,diff,loc,msg,significant) ->
+              (fun (env,diff,loc_msg,significant) ->

                 let env' =
                  filter_map_domain
                    (fun locs domain_item ->
                 let env' =
                  filter_map_domain
                    (fun locs domain_item ->


@@ -1140,19 +1305,19 @@ in refine_profiler.HExtlib.profile foo ()
                       Not_found -> None)
                    thing_dom
                 in
                       Not_found -> None)
                    thing_dom
                 in

-                 env',diff,loc,msg,significant
+                 env',diff,loc_msg,significant

               ) errors
             in
              raise (NoWellTypedInterpretation (0,errors))
               ) errors
             in
              raise (NoWellTypedInterpretation (0,errors))

-         | [_,diff,metasenv,t,ugraph],_,_ ->
+         | [_,diff,metasenv,subst,t,ugraph],_,_ ->

              debug_print (lazy "SINGLE INTERPRETATION");
              debug_print (lazy "SINGLE INTERPRETATION");

-             [diff,metasenv,t,ugraph], false
+             [diff,metasenv,subst,t,ugraph], false

          | l,_,_ ->
              debug_print 
                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
          | l,_,_ ->
              debug_print 
                (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map

-                 (fun (env, _, _, _, _) ->
+                 (fun (env, _, _, _, _, _) ->

                    map_domain
                      (fun locs domain_item ->
                        let description =
                    map_domain
                      (fun locs domain_item ->
                        let description =


@@ -1166,7 +1331,8 @@ in refine_profiler.HExtlib.profile foo ()
                C.interactive_interpretation_choice 
                  thing_txt thing_txt_prefix_len choices 
              in
                C.interactive_interpretation_choice 
                  thing_txt thing_txt_prefix_len choices 
              in

-             (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
+             (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
+               choosed),

               true
         in
          res
               true
         in
          res


@@ -1174,18 +1340,37 @@ in refine_profiler.HExtlib.profile foo ()
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"
 
       CicEnvironment.CircularDependency s -> 
         failwith "Disambiguate: circular dependency"
 

-    let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe 
+    let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv 
+      ~subst ?goal
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 

       (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in
       (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
       in

-      disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
+      let hint = match goal with
+        | None -> (fun _ x -> x), fun k -> k
+        | Some i ->
+            (fun metasenv t ->
+              let _,c,ty = CicUtil.lookup_meta i metasenv in
+              assert(c=context);
+              Cic.Cast(t,ty)),
+            function  
+            | Ok (t,m,s,ug) ->
+                (match t with
+                | Cic.Cast(t,_) -> Ok (t,m,s,ug)
+                | _ -> assert false) 
+            | k -> k
+      in
+      let localization_tbl = Cic.CicHash.create 503 in
+       disambiguate_thing ~dbd ~context ~metasenv ~subst
+        ~initial_ugraph ~aliases

         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term

-        ~interpretate_thing:interpretate_term
+        ~interpretate_thing:(interpretate_term (?create_dummy_ids:None))

         ~refine_thing:refine_term (text,prefix_len,term)
         ~refine_thing:refine_term (text,prefix_len,term)

+        ~localization_tbl
+        ~hint

 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
      (text,prefix_len,obj)
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
      (text,prefix_len,obj)


@@ -1193,9 +1378,20 @@ in refine_profiler.HExtlib.profile foo ()
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in

-      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
+      let hint = 
+        (fun _ x -> x),
+        fun k -> k
+      in
+      let localization_tbl = Cic.CicHash.create 503 in
+      disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[] 
+        ~aliases ~universe ~uri

         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
         ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj

+        ~initial_ugraph:CicUniv.empty_ugraph

         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj

+        ~localization_tbl
+        ~hint

         (text,prefix_len,obj)
         (text,prefix_len,obj)

+

   end
 
   end
 

+