Backport from opam repo

C.f. coq/opam#3293

(cherry picked from commit 4495ca0)

coq-core.opam

@@ -2,6 +2,20 @@
 opam-version: "2.0"
 version: "dev"
 synopsis: "Compatibility binaries for Coq after the Rocq renaming"
+description: """
+The Rocq Prover is an interactive theorem prover, or proof assistant. 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 compatibility binaries to call Rocq
+through previous Coq commands like coqc coqtop,..."""
 maintainer: ["The Rocq development team <[email protected]>"]
 authors: ["The Rocq development team, INRIA, CNRS, and contributors"]
 license: "LGPL-2.1-only"

dune-project

@@ -30,6 +30,9 @@
   (ocamlfind (>= 1.8.1))
   (zarith (>= 1.11))
   (conf-linux-libc-dev (= :os "linux")))
+ (conflicts
+  (coq (< 8.17))
+  (coq-core (< 8.21)))
  (depopts rocq-native memprof-limits memtrace)
  (synopsis "The Rocq Prover -- Core Binaries and Tools")
  (description "The Rocq Prover is an interactive theorem prover, or proof assistant. It provides
@@ -54,7 +57,20 @@ prelude, now living in the rocq-core package."))
  (name coq-core)
  (depends
   (rocq-runtime (= :version)))
- (synopsis "Compatibility binaries for Coq after the Rocq renaming"))
+ (synopsis "Compatibility binaries for Coq after the Rocq renaming")
+ (description "The Rocq Prover is an interactive theorem prover, or proof assistant. 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 compatibility binaries to call Rocq
+through previous Coq commands like coqc coqtop,..."))
 
 (package
  (name rocq-core)

rocq-runtime.opam

@@ -35,6 +35,10 @@ depends: [
   "odoc" {with-doc}
 ]
 depopts: ["rocq-native" "memprof-limits" "memtrace"]
+conflicts: [
+  "coq" {< "8.17"}
+  "coq-core" {< "8.21"}
+]
 dev-repo: "git+https://github.com/coq/coq.git"
 build: [
   ["dune" "subst"] {dev}