rocq-micromega-plugin 1.1.0-1
Package Information
| Description | Semi-decision procedures for arithmetic in Rocq Rocq is a proof asssistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5. This package provides a plugin to Rocq providing (semi-)decision procedures for arithmetic ; end-users can use it through various tactics like 'lra'. |
|---|---|
| Maintainer | Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org> |
| Changed By | Julien Puydt <jpuydt@debian.org> |
| Sponsor | jpuydt@debian.org |
| Distribution | experimental |
| Architecture | any |
| VCS | git: https://salsa.debian.org/ocaml-team/rocq-micromega-plugin.git (browse) |
| Closes | #1142096 |
| Tracker | https://tracker.debian.org/pkg/rocq-micromega-plugin |
| Uploaded | 2 hours ago |
New Package Report
.changes
| Architecture | source amd64 |
|---|---|
| Distribution | experimental |
| Date | Thu, 16 Jul 2026 14:47:45 +0200 |
| Source | rocq-micromega-plugin |
| Version | 1.1.0-1 |
| Changed-By | Julien Puydt |
Changelog
rocq-micromega-plugin (1.1.0-1) experimental; urgency=medium . * Initial release. (Closes: #1142096)
.dsc
| Priority | optional |
|---|---|
| Component | main |
| Package-List | libcoq-micromega-plugin deb math optional arch=any |
| Section | math |
debian/copyright
Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ Upstream-Name: rocq-micromega-plugin Source: https://github.com/rocq-community/micromega-plugin Files: * Copyright: INRIA, CNRS and contributors 2006-2026 Frédéric Besson License: LGPL-2.1 Files: debian/* Copyright: 2026 Julien Puydt License: LGPL-2.1 License: LGPL-2.1 This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License, version 2.1, as published by the Free Software Foundation. . This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more details. . On Debian systems, the complete text of the GNU Lesser General Public License version 2.1 can be found in "/usr/share/common-licenses/LGPL-2.1".