63 lines
1.7 KiB
Ruby
63 lines
1.7 KiB
Ruby
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'
|
|
|
|
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
|