1 files changed, 46 insertions, 7 deletions

diff --git a/dune-project b/dune-project
index 03e7147019..251fbd92aa 100644
--- a/dune-project
+++ b/dune-project
@@ -22,14 +22,13 @@
 ; Note that we use coq.opam.template to have dune add the correct opam
 ; prefix for configure
 (package
- (name coq)
+ (name coq-core)
  (depends
   (ocaml (>= 4.05.0))
-  (dune  (>= 2.5.0))
   (ocamlfind (>= 1.8.1))
   (zarith (>= 1.10))
   (ounit2 :with-test))
- (synopsis "The Coq Proof Assistant")
+ (synopsis "The Coq Proof Assistant -- Core Binaries and Tools")
  (description "Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
 algorithms and theorems together with an environment for
@@ -39,13 +38,38 @@ Typical applications include the certification of properties of
 programming languages (e.g. the CompCert compiler certification
 project, or the Bedrock verified low-level programming library), the
 formalization of mathematics (e.g. the full formalization of the
-Feit-Thompson theorem or homotopy type theory) and teaching."))
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq core binaries, plugins, and tools, but
+not the vernacular standard library.
+
+Note that in this setup, Coq needs to be started with the -boot and
+-noinit options, as will otherwise fail to find the regular Coq
+prelude, now living in the coq-stdlib package."))
+
+(package
+ (name coq-stdlib)
+ (depends
+  (coq-core (= :version)))
+ (synopsis "The Coq Proof Assistant -- Standard Library")
+ (description "Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching.
+
+This package includes the Coq Standard Library, that is to say, the
+set of modules usually bound to the Coq.* namespace."))
 
 (package
  (name coqide-server)
  (depends
-  (dune (>= 2.5.0))
-  (coq (= :version)))
+  (coq-core (= :version)))
  (synopsis "The Coq Proof Assistant, XML protocol server")
  (description "Coq is a formal proof management system. It provides
 a formal language to write mathematical definitions, executable
@@ -60,7 +84,6 @@ structured way."))
 (package
  (name coqide)
  (depends
-  (dune (>= 2.5.0))
   (coqide-server (= :version)))
  (synopsis "The Coq Proof Assistant --- GTK3 IDE")
  (description "Coq is a formal proof management system. It provides
@@ -86,3 +109,19 @@ semi-interactive development of machine-checked proofs.
 
 This package provides the Coq Reference Manual."))
 
+(package
+ (name coq)
+ (depends
+  (coq-core (= :version))
+  (coq-stdlib (= :version)))
+ (synopsis "The Coq Proof Assistant")
+ (description "Coq is a formal proof management system. It provides
+a formal language to write mathematical definitions, executable
+algorithms and theorems together with an environment for
+semi-interactive development of machine-checked proofs.
+
+Typical applications include the certification of properties of
+programming languages (e.g. the CompCert compiler certification
+project, or the Bedrock verified low-level programming library), the
+formalization of mathematics (e.g. the full formalization of the
+Feit-Thompson theorem or homotopy type theory) and teaching."))