X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=47ca04debbacd9f30074584da5ff48f99418c78e;hb=c1564f164c3acee3b74593ebc2154d718db7856b;hp=d8af6b10e566bb8e3e2c46c9881e6adaf8edaac1;hpb=16065a413f4be50761d73be9dca3953ff9bfc1eb;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index d8af6b10e..47ca04deb 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -36,8 +36,8 @@ exception Invalid_action of string  (* invalid action for "/search" method *)
   (** raised by elim when a MutInd is required but not found *)
 exception Not_a_MutInd
 
-let daemon_name = "Moogle"
-let configuration_file = "/projects/helm/etc/moogle.conf.xml"
+let daemon_name = "Whelp"
+let configuration_file = "/projects/helm/etc/whelp.conf.xml"
 
 let placeholders = [
   "ACTION"; "ADVANCED"; "ADVANCED_CHECKED"; "CHOICES"; "CURRENT_CHOICES";
@@ -323,7 +323,8 @@ let exec_action dbd (req: Http_types.request) outchan =
     let ast = CicTextualParser2.parse_term (Stream.of_string term_str) in
     let (id_to_uris, metasenv, term) =
       match
-        Disambiguate'.disambiguate_term dbd context metasenv ast id_to_uris
+        Disambiguate'.disambiguate_term ~dbd ~context ~metasenv
+          ~aliases:id_to_uris ast
       with
       | [id_to_uris,metasenv,term,_] -> id_to_uris,metasenv,term
       | _ -> assert false
@@ -338,7 +339,7 @@ let exec_action dbd (req: Http_types.request) outchan =
           (match subgoals with
           | proof, [goal] ->
               let (uri,metasenv,bo,ty) = proof in
-              List.map fst (MetadataQuery.hint ~dbd (proof, goal))
+              List.map fst (MetadataQuery.experimental_hint ~dbd (proof, goal))
           | _ -> assert false)
       | "/elim" ->
           let uri =