diff --git a/Aliases/mathcomp b/Aliases/mathcomp
new file mode 120000
index 0000000000..51eb61d337
--- /dev/null
+++ b/Aliases/mathcomp
@@ -0,0 +1 @@
+../Formula/math-comp.rb
\ No newline at end of file
diff --git a/Aliases/ssreflect b/Aliases/ssreflect
new file mode 120000
index 0000000000..51eb61d337
--- /dev/null
+++ b/Aliases/ssreflect
@@ -0,0 +1 @@
+../Formula/math-comp.rb
\ No newline at end of file
diff --git a/Formula/math-comp.rb b/Formula/math-comp.rb
new file mode 100644
index 0000000000..320087a79e
--- /dev/null
+++ b/Formula/math-comp.rb
@@ -0,0 +1,46 @@
+class MathComp < Formula
+  desc "Mathematical Components for the Coq proof assistant"
+  homepage "https://math-comp.github.io/math-comp/"
+  url "https://github.com/math-comp/math-comp/archive/mathcomp-1.6.4.tar.gz"
+  sha256 "c672a4237f708b5f03f1feed9de37f98ef5c331819047e1f71b5762dcd92b262"
+  head "https://github.com/math-comp/math-comp.git"
+
+  depends_on "ocaml" => :build
+  depends_on "coq"
+
+  def install
+    coqbin = "#{Formula["coq"].opt_bin}/"
+    coqlib = "#{lib}/coq/"
+
+    (buildpath/"mathcomp/Makefile.coq.local").write <<~EOS
+      COQLIB=#{coqlib}
+    EOS
+
+    cd "mathcomp" do
+      system "make", "MAKEFLAGS=#{ENV["MAKEFLAGS"]}", "COQBIN=#{coqbin}"
+      system "make", "install", "MAKEFLAGS=#{ENV["MAKEFLAGS"]}", "COQBIN=#{coqbin}"
+
+      elisp.install "ssreflect/pg-ssr.el"
+    end
+
+    system "make", "-C", "htmldoc", "COQBIN=#{coqbin}" if build.head?
+
+    doc.install Dir["htmldoc/*"]
+  end
+
+  test do
+    (testpath/"testing.v").write <<~EOS
+      From mathcomp Require Import ssreflect seq.
+
+      Parameter T: Type.
+      Theorem test (s1 s2: seq T): size (s1 ++ s2) = size s1 + size s2.
+      Proof. by elim : s1 =>//= x s1 ->. Qed.
+
+      Check test.
+    EOS
+
+    coqc = Formula["coq"].opt_bin/"coqc"
+    cmd = "#{coqc} -R #{lib}/coq/user-contrib/mathcomp mathcomp testing.v"
+    assert_match /\Atest\s+: forall/, shell_output(cmd)
+  end
+end
diff --git a/Formula/ssreflect.rb b/Formula/ssreflect.rb
deleted file mode 100644
index f246bac574..0000000000
--- a/Formula/ssreflect.rb
+++ /dev/null
@@ -1,125 +0,0 @@
-class Camlp5TransitionalModeRequirement < Requirement
-  fatal true
-
-  satisfy(:build_env => false) { !Tab.for_name("camlp5").with?("strict") }
-
-  def message; <<~EOS
-    camlp5 must be compiled in transitional mode (instead of --strict mode):
-      brew install camlp5
-    EOS
-  end
-end
-
-class Ssreflect < Formula
-  desc "Virtual package provided by libssreflect-coq"
-  homepage "https://math-comp.github.io/math-comp/"
-  url "http://ssr.msr-inria.inria.fr/FTP/ssreflect-1.5.tar.gz"
-  sha256 "bad978693d1bfd0a89586a34678bcc244e3b7efba6431e0f83d8e1ae8f82a142"
-  revision 3
-
-  bottle do
-    sha256 "952d4dbbbb3599a901814892769fd42b2a86fc72544100d7abba42fbca56df0f" => :high_sierra
-    sha256 "d2bb5472dc0339957be0f11efe89fdc9c367a0ab0d4458cb80c7829eec31fd7d" => :sierra
-    sha256 "8bb36558561b6e9f95f65f13278add1cb5aaec4596b7b9010fc1abbaa4fc049d" => :el_capitan
-    sha256 "4e818fc061186ff528dea4aae58db36fb8358152527185f6150b71cdf2b4c598" => :yosemite
-  end
-
-  option "with-doc", "Install HTML documents"
-  option "without-static", "Build without static linking"
-
-  depends_on "ocaml"
-  depends_on "menhir" => :build
-  depends_on "camlp5" => :build # needed for building Coq 8.4
-  depends_on Camlp5TransitionalModeRequirement # same requirement as in Coq formula
-
-  resource "coq84" do
-    url "https://coq.inria.fr/distrib/V8.4pl6/files/coq-8.4pl6.tar.gz"
-    sha256 "a540a231a9970a49353ca039f3544616ff86a208966ab1c593779ae13c91ebd6"
-  end
-
-  # Fix an ill-formatted ocamldoc comment.
-  patch :DATA
-
-  def install
-    ENV["OCAMLPARAM"] = "safe-string=0,_" # OCaml 4.06.0 compat
-
-    resource("coq84").stage do
-      system "./configure", "-prefix", libexec/"coq",
-                            "-camlp5dir", Formula["camlp5"].opt_lib/"ocaml/camlp5",
-                            "-coqide", "no",
-                            "-with-doc", "no",
-                            # Prevent warning 31 (module is linked twice in the
-                            # same executable) from being a fatal error, which
-                            # would otherwise be the default as of ocaml 4.03.0;
-                            # note that "-custom" is the default value of
-                            # coqrunbyteflags, and is necessary, so don't just
-                            # overwrite it with "-warn-error -a"
-                            "-coqrunbyteflags", "-warn-error -a -custom"
-
-      system "make", "VERBOSE=1", "world"
-      ENV.deparallelize { system "make", "install" }
-    end
-
-    ENV.prepend_path "PATH", libexec/"coq/bin"
-    ENV.deparallelize
-
-    # Enable static linking.
-    if build.with? "static"
-      inreplace "Make" do |s|
-        s.gsub! /#\-custom/, "-custom"
-        s.gsub! /#SSRCOQ/, "SSRCOQ"
-      end
-    end
-
-    args = %W[
-      COQBIN=#{libexec}/coq/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"
-    pkgshare.install "pg-ssr.el"
-  end
-
-  test do
-    (testpath/"helloworld.v").write <<~EOS
-      Add LoadPath "#{lib}/coq/user-contrib/Ssreflect" as Ssreflect.
-      Require Import Ssreflect.ssreflect.
-      Variable P:Prop.
-
-      Theorem helloworld: P -> P.
-      Proof.
-        done.
-      Qed.
-
-      Check helloworld.
-    EOS
-    (testpath/"expected").write <<~EOS
-      helloworld
-           : P -> P
-    EOS
-    assert_equal File.read(testpath/"expected"), pipe_output("#{bin}/ssrcoq -compile helloworld")
-  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
diff --git a/formula_renames.json b/formula_renames.json
index 7308bfd202..e1fc7ddcfc 100644
--- a/formula_renames.json
+++ b/formula_renames.json
@@ -165,6 +165,7 @@
   "sonar": "sonarqube",
   "speedtest_cli": "speedtest-cli",
   "srtp@1.5": "srtp@1.6",
+  "ssreflect": "math-comp",
   "stash-cli": "atlassian-cli",
   "subversion18": "subversion@1.8",
   "swig2": "swig@2",