X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2FsearchEngine%2FmooglePp.ml;h=3af0afb4051f882f5251d44891ecc787c93cc232;hb=ce3b9018fe80437a56e56f2bc0b5696b2acb59bb;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 "