|
1 |
| -# mczify |
| 1 | +<!--- |
| 2 | +This file was generated from `meta.yml`, please do not edit manually. |
| 3 | +Follow the instructions on https://github.com/coq-community/templates to regenerate. |
| 4 | +---> |
| 5 | +# Mczify |
| 6 | + |
| 7 | +[![Docker CI][docker-action-shield]][docker-action-link] |
| 8 | + |
| 9 | +[docker-action-shield]: https://github.com/math-comp/mczify/workflows/Docker%20CI/badge.svg?branch=master |
| 10 | +[docker-action-link]: https://github.com/math-comp/mczify/actions?query=workflow:"Docker%20CI" |
| 11 | + |
| 12 | + |
| 13 | + |
| 14 | + |
| 15 | +This small library enables the use of the Micromega tactics for goals stated |
| 16 | +with the definitions of the Mathematical Components library by extending the |
| 17 | +zify tactic. |
| 18 | + |
| 19 | +## Meta |
| 20 | + |
| 21 | +- Author(s): |
| 22 | + - Kazuhiko Sakaguchi (initial) |
| 23 | +- License: [CeCILL-B Free Software License Agreement](CeCILL-B) |
| 24 | +- Compatible Coq versions: 8.13 or later |
| 25 | +- Additional dependencies: |
| 26 | + - [MathComp](https://math-comp.github.io) 1.12.0 or later |
| 27 | +- Coq namespace: `mathcomp.zify` |
| 28 | +- Related publication(s): none |
| 29 | + |
| 30 | +## Building and installation instructions |
| 31 | + |
| 32 | +The easiest way to install the latest released version of Mczify |
| 33 | +is via [OPAM](https://opam.ocaml.org/doc/Install.html): |
| 34 | + |
| 35 | +```shell |
| 36 | +opam repo add coq-released https://coq.inria.fr/opam/released |
| 37 | +opam install coq-mathcomp-zify |
| 38 | +``` |
| 39 | + |
| 40 | +To instead build and install manually, do: |
| 41 | + |
| 42 | +``` shell |
| 43 | +git clone https://github.com/math-comp/mczify.git |
| 44 | +cd mczify |
| 45 | +make # or make -j <number-of-cores-on-your-machine> |
| 46 | +make install |
| 47 | +``` |
| 48 | + |
2 | 49 |
|
3 |
| -## Requirements |
4 | 50 |
|
5 |
| -- Coq 8.13 or later, and |
6 |
| -- Mathematical Components 1.12.0 or later. |
|
0 commit comments