Permalink
Browse files

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>
  • Loading branch information...
1 parent d2317c9 commit b44f8e62acffc29e6cd8da5d782da97d6dee0e15 @mht208 mht208 committed with adamv Sep 10, 2012
Showing with 62 additions and 0 deletions.
  1. +62 −0 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

0 comments on commit b44f8e6

Please sign in to comment.