require 'formula'

class Ssreflect < Formula
  homepage 'http://www.msr-inria.inria.fr/Projects/math-components'
  url 'http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.4-coq8.4.tar.gz'
  version '1.4'
  sha1 'c9e678a362973b202a5d90d2abf6436fa1ab4dcf'

  depends_on 'objective-caml'
  depends_on 'coq'

  option 'with-doc', 'Install HTML documents'
  option 'with-static', 'Build with static linking'

  # Fix an ill-formatted ocamldoc comment.
  patch :DATA

  def install
    ENV.j1

    # Enable static linking.
    if build.with? "static"
      inreplace 'Make' do |s|
        s.gsub! /#\-custom/, '-custom'
        s.gsub! /#SSRCOQ/, 'SSRCOQ'
      end
    end

    args = ["COQBIN=#{HOMEBREW_PREFIX}/bin/",
            "COQLIBINSTALL=lib/coq/user-contrib",
            "COQDOCINSTALL=share/doc",
            "DSTROOT=#{prefix}/"]
    system "make", *args
    system "make", "install", *args
    if build.with? "doc"
      system "make", "-f", "Makefile.coq", "html", *args
      system "make", "-f", "Makefile.coq", "mlihtml", *args
      system "make", "-f", "Makefile.coq", "install-doc", *args
    end
    bin.install 'bin/ssrcoq.byte', 'bin/ssrcoq' if build.with? "static"
    (share/'ssreflect').install "pg-ssr.el"
  end

end


__END__
diff --git a/src/ssrmatching.mli b/src/ssrmatching.mli
index fd2e835..1d9d15b 100644
--- a/src/ssrmatching.mli
+++ b/src/ssrmatching.mli
@@ -77,7 +77,7 @@ val interp_cpattern :
     pattern

 (** The set of occurrences to be matched. The boolean is set to true
- *  to signal the complement of this set (i.e. {-1 3}) *)
+ *  to signal the complement of this set (i.e. \{-1 3\}) *)
 type occ = (bool * int list) option

 (** Substitution function. The [int] argument is the number of binders