X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FsearchEngine.ml;h=655235c1e538121ca0b72bc124a90bc47db2b139;hb=03b76418d261acfb3b33d64283ea0269ba596859;hp=47ca04debbacd9f30074584da5ff48f99418c78e;hpb=e5050c8f2f36a4d697e3a7c5b24ecc1d5dc73f48;p=helm.git

diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml
index 47ca04deb..655235c1e 100644
--- a/helm/searchEngine/searchEngine.ml
+++ b/helm/searchEngine/searchEngine.ml
@@ -126,6 +126,7 @@ let query_kind_of_req (req: Http_types.request) =
   | "/hint" -> "Hint"
   | "/locate" -> "Locate"
   | "/elim" -> "Elim"
+  | "/instance" -> "Instance"
   | _ -> ""
 
   (* given a uri with a query part in input try to find in it a string
@@ -332,6 +333,7 @@ let exec_action dbd (req: Http_types.request) outchan =
     let uris =
       match req#path with
       | "/match" -> MetadataQuery.match_term ~dbd term
+      | "/instance" -> MetadataQuery.instance ~dbd term
       | "/hint" ->
           let status = ProofEngineTypes.initial_status term metasenv in
           let intros = PrimitiveTactics.intros_tac () in
@@ -410,6 +412,7 @@ let callback dbd (req: Http_types.request) outchan =
         end
     | "/hint"
     | "/elim"
+    | "/instance"
     | "/match" -> exec_action dbd req outchan
     | invalid_request ->
         Http_daemon.respond_error ~code:(`Status (`Client_error `Bad_request))