X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=9f4c41d2e709e608b5f7497d27692d6737736598;hb=0aaed6f96b856d1181a3cd1f2ef3ea4a91990771;hp=b36ae5b119ecba762c529f79baeb52181f987fb8;hpb=3d45448d06307244c530a9e52d33e4a3723eec55;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b36ae5b11..9f4c41d2e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -67,13 +67,11 @@ let refine metasenv context term ugraph =
 	(Ok (term', metasenv')),ugraph1
     with
       | CicRefine.Uncertain _ ->
-          debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+          debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
           Uncertain,ugraph
       | CicRefine.RefineFailure msg ->
-          debug_print (
-            (sprintf ("%%%%%% PRUNED!!!\n<<begin cause>>\n" ^^ 
-              "%s\n<<end cause>>\n<<begin term>>\n%s\n<<end term>>") 
-              msg (CicPp.ppterm term)));
+          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+            (CicPp.ppterm term) msg);
           Ko,ugraph
       | CicUnification.UnificationFailure s -> 
 	 prerr_endline ("PASSADI QUI: " ^ s);
@@ -421,8 +419,8 @@ let domain_diff dom1 dom2 =
 
 module Make (C: Callbacks) =
   struct
-    let choices_of_id ?owner dbd id =
-      let uris = MetadataQuery.locate ?owner ~dbd id in
+    let choices_of_id dbd id =
+      let uris = MetadataQuery.locate ~dbd id in
       let uris =
        match uris with
         | [] ->
@@ -452,7 +450,7 @@ module Make (C: Callbacks) =
         uris
 
     let disambiguate_term ~(dbd:Mysql.dbd) context metasenv term
-      ?(initial_ugraph = CicUniv.empty_ugraph) ?owner ~aliases:current_env
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases:current_env
     =
       debug_print "NEW DISAMBIGUATE INPUT";
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -477,7 +475,7 @@ module Make (C: Callbacks) =
               (try
                 Hashtbl.find id_choices id
               with Not_found ->
-                let choices = choices_of_id ?owner dbd id in
+                let choices = choices_of_id dbd id in
                 Hashtbl.add id_choices id choices;
                 choices)
           | Symbol (symb, _) -> DisambiguateChoices.lookup_symbol_choices symb