X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FsearchEngine%2FmooglePp.ml;h=3af0afb4051f882f5251d44891ecc787c93cc232;hb=7a7af8e1ed42aa440476975ec918d38f0c3d13c9;hp=dd3b63ded91ba40e5f8d436a519b26258e486e9a;hpb=8ad6f4591d80a263510d516f4b5bc0d75aabd81c;p=helm.git diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml index dd3b63ded..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 "