X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FsearchEngine%2FmooglePp.ml;h=3af0afb4051f882f5251d44891ecc787c93cc232;hb=0c04e1f673d69ac652c15705863931c45e107515;hp=998274e08525e60bd7d38a297d210ea1ae419d87;hpb=5cb2fa1e3e6f5d9d7a273b45c56a6c1196982c4a;p=helm.git diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml index 998274e08..3af0afb40 100644 --- a/helm/searchEngine/mooglePp.ml +++ b/helm/searchEngine/mooglePp.ml @@ -1,16 +1,8 @@ open Printf -let pp_request (req: Http_types.request) = - match req#path with - | "/elim" -> "Elim" - | "/match" -> "Match" - | "/hint" -> "Hint" - | "/locate" -> "Locate" - | _ -> assert false - let pp_error title msg = - sprintf "