X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=f7cfce144d7b6daacbceaafdc16ef71cdbc4286d;hb=b4a7a577a04c56a68b6d79d06fdb925ff0bbd331;hp=6a6ab9b274333529b8df915bb40f09fee54baa5f;hpb=de34baf0da4b2d4e50eba307e86d518bb3a071cc;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 6a6ab9b27..f7cfce144 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -57,8 +57,7 @@ let refine metasenv context term =
     | CicRefine.Uncertain _ ->
         debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
         Uncertain
-    | _ ->
-        (* TODO we should catch only the RefineFailure excecption *)
+    | CicRefine.RefineFailure _ ->
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
@@ -258,7 +257,7 @@ let interpretate ~context ~env ast =
         Cic.Meta (index, cic_subst)
     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
     | CicAst.Sort `Set -> Cic.Sort Cic.Set
-    | CicAst.Sort `Type -> Cic.Sort Cic.Type
+    | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
@@ -404,18 +403,11 @@ module Make (C: Callbacks) =
        (function uri,_ ->
          MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri
        ) result in
-      HelmLogger.log (`Msg (`T "Locate query:"));
-      MQueryUtil.text_of_query
-       (fun s -> HelmLogger.log ~append_NL:false (`Msg (`T s)))
-       "" query; 
-      HelmLogger.log (`Msg (`T "Result:"));
-      MQueryUtil.text_of_result
-        (fun s -> HelmLogger.log (`Msg (`T s))) "" result;
       let uris' =
        match uris with
         | [] ->
            [UriManager.string_of_uri (C.input_or_locate_uri
-            ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+            ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
         | [uri] -> [uri]
         | _ ->
             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE