Address opam archive review: rename, drop ocaml dep, fix maintainer

[grootstebozewolf]

Review on rocq-prover/opam#3829 from proux01 — "A few comments but otherwise LGTM." Three fixed, one declined with a reason.

1. Rename → rocq-robust-geometric-predicates

"robust-predicates seems a bit overly generic" / "geometric seems like a very important keyword here"

Agreed — the discriminating word was only in the synopsis. Free now, impossible after the archive entry merges. Directory, opam file, workflow, MANIFEST, dune stanzas, nix pname and release script all move together; theories/dune's (package ...) must match the opam filename or dune fails, so a partial rename would break the build rather than pass quietly.

2. Drop the ocaml dependency (both packages)

"Does this really need ocaml? I don't see any ml code in the tarball."

He's right, and I verified it: zero .ml/.mli/.mll/.mly files in either tarball, and the Makefile's only ocaml/dune mentions are a tar file list and a comment. The build is pure rocq makefile. I had copied this from rocq-bignums, which genuinely ships OCaml — we don't, so it was an unearned dependency.

3. Fix maintainer (both packages)

"The maintainer OPAM field is the maintainer of the package (so yourself…)"

Was an issue-tracker URL, now a person. bug-reports already carries the tracker URL.

4. Declined — mentioning JTS in the description

"Should this say anything about JTS? (I'm not sure how important the link is)"

The package is standalone Rocq with no JTS dependency, and a Rocq user installing it needs nothing about Java geometry libraries. homepage already leads anyone curious to the corpus. Recorded here so the decision is visible rather than silently skipped.

Also

Trimmed the long coq-flocq rationale in the repo copy to the three-line version already submitted upstream, so the two no longer diverge.

Verified

21 files assemble, make clean, opam lint Passed under the new name.

Next, after this merges

rocq-robust-predicates 0.1.0 is already published with a tarball whose internal opam file carries the old name. Rather than point the renamed archive entry at a mismatched tarball, I'll cut rocq-robust-geometric-predicates-v0.1.0 and update #3829 with the new URL and checksum. rocq-spatial-algebra 0.1.0 is unaffected — its tarball and archive entry stand as published, and only its maintainer/ocaml lines change.

topics: packaging, opam
witness: assemble + make + opam lint clean under the new name
claimId: n/a (packaging)