From 4e3b992c548ec5c1bc89cd6c2878f30ddbda32c9 Mon Sep 17 00:00:00 2001
From: Ming-Hsien Tsai
Date: Mon, 10 Sep 2012 23:43:38 +0800
Subject: Ssreflect 1.4

Ssreflect is an extension of Coq. It provides convenient notations,
several mathematical components, and other general purpose features.
The famous Four Colour Theorem was proved in Coq with the Ssreflect
extension.

Closes #14836.

Signed-off-by: Adam Vandenberg <flangy@gmail.com>
---
 Library/Formula/ssreflect.rb | 62 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)
 create mode 100644 Library/Formula/ssreflect.rb

(limited to 'Library')

diff --git a/Library/Formula/ssreflect.rb b/Library/Formula/ssreflect.rb
new file mode 100644
index 000000000..219eb2979
--- /dev/null
+++ b/Library/Formula/ssreflect.rb
@@ -0,0 +1,62 @@
+require 'formula'
+
+class Ssreflect < Formula
+  homepage 'http://www.msr-inria.inria.fr/Projects/math-components'
+  url 'http://www.msr-inria.inria.fr/Projects/math-components/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'
+
+  def patches
+    # Fix an ill-formatted ocamldoc comment.
+    DATA
+  end
+
+  def install
+    ENV.j1
+
+    # Enable static linking.
+    if build.include? '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.include? '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.include? '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
-- 
cgit v1.2.3