fix after @silene comments

Author: tabareau

core-dev/packages/coqide-server/coqide-server.9.2.dev/opam

@@ -1,21 +1,15 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "dev"
-synopsis: "Compatibility binaries for Coq after the Rocq renaming"
+synopsis: "The Rocq Prover, XML protocol server"
 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,..."""
+This package provides the `coqidetop` language server, an
+implementation of Rocq's [XML protocol](https://github.com/rocq-prover/rocq/blob/master/dev/doc/xml-protocol.md)
+which allows clients, such as RocqIDE, to interact with the Rocq Prover in a
+structured way."""
 maintainer: [
   "The Rocq development team <rocq+rocq-development@discoursemail.com>"
 ]
@@ -44,10 +38,6 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/rocq-prover/rocq.git"
-post-messages: [
-  "Coq has been renamed to The Rocq Prover, see https://rocq-prover.org/refman/changes.html#porting-to-the-rocq-prover for details. 
-   This package provides compatibility binaries to ease the transition to the new rocq binary."
-]
 url {
   src: "git+https://github.com/coq/coq.git#v9.2"
 }

core-dev/packages/rocq-core/rocq-core.9.2.dev/opam

@@ -1,6 +1,4 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "dev"
 synopsis: "The Rocq Prover with its prelude"
 description: """
 The Rocq Prover is an interactive theorem prover, or proof assistant. It provides

core-dev/packages/rocq-runtime/rocq-runtime.9.2.dev/opam

@@ -1,6 +1,4 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "dev"
 synopsis: "The Rocq Prover -- Core Binaries and Tools"
 description: """
 The Rocq Prover is an interactive theorem prover, or proof assistant. It provides