X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FsearchEngine%2FmooglePp.ml;h=3af0afb4051f882f5251d44891ecc787c93cc232;hb=6f0e3275c5a100568c8529d6c58150ef4af692d0;hp=50809a45940bc9f05383d2c70c9298df8e9aea00;hpb=3f6f868f14eadef7f17d5e3008cffe19307ad492;p=helm.git diff --git a/helm/searchEngine/mooglePp.ml b/helm/searchEngine/mooglePp.ml index 50809a459..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 "