Bug#1142096: ITP: rocq-micromega-plugin -- Semi-decision procedures for arithmetic in Rocq

Julien Puydt <[email protected]> Wed, 15 Jul 2026 10:56:53 +0200

Newsgroups	gmane.linux.debian.devel.general
Message-ID	<178410581399.3341528.14133317335084206153.reportbug__14798.9553793863$1784105974$gmane$org@efrim>

Package: wnpp
Severity: wishlist
Owner: Julien Puydt <[email protected]>
X-Debbugs-Cc: [email protected], [email protected], [email protected]

* Package name    : rocq-micromega-plugin
  Version         : 1.1.0-1
  Upstream Contact: Pierre Roux <[email protected]>
* URL             : https://github.com/rocq-community/micromega-plugin/
* License         : LGPL-2.1
  Programming Lang: OCaml
  Description     : Semi-decision procedures for arithmetic in Rocq
 This package provides a plugin to Rocq providing (semi-)decision
 procedures for arithmetic ; end-users can use it through various
 tactics like 'lra'.

This package is a new dependency of mathcomp/ssreflect, already
packaged in Debian. I plan to maintain it within the
Debian-Ocaml-Maintainers team along with the rest of the Coq/Rocq
packages.

Cheers,

J.Puydt