From 899e650212a77e32d85c85cea32e6aafbd3514c4 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 28 Sep 2021 21:45:34 +0900 Subject: [PATCH] Update doc --- README.md | 8 +++++--- coq-mathcomp-zify.opam | 8 +++++--- meta.yml | 8 +++++--- 3 files changed, 15 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index f16b73f..a6add66 100644 --- a/README.md +++ b/README.md @@ -12,9 +12,11 @@ Follow the instructions on https://github.com/coq-community/templates to regener -This small library enables the use of the Micromega tactics for goals stated -with the definitions of the Mathematical Components library by extending the -zify tactic. +This small library enables the use of the Micromega arithmetic solvers of Coq +for goals stated with the definitions of the Mathematical Components library +by extending the zify tactic. Other than that, the `ssrZ` library provides +some basic MathComp style definitions to reason about the standard integer +type `Z`. ## Meta diff --git a/coq-mathcomp-zify.opam b/coq-mathcomp-zify.opam index e8e42ce..b1c6982 100644 --- a/coq-mathcomp-zify.opam +++ b/coq-mathcomp-zify.opam @@ -12,9 +12,11 @@ license: "CECILL-B" synopsis: "Micromega tactics for Mathematical Components" description: """ -This small library enables the use of the Micromega tactics for goals stated -with the definitions of the Mathematical Components library by extending the -zify tactic.""" +This small library enables the use of the Micromega arithmetic solvers of Coq +for goals stated with the definitions of the Mathematical Components library +by extending the zify tactic. Other than that, the `ssrZ` library provides +some basic MathComp style definitions to reason about the standard integer +type `Z`.""" build: [make "-j%{jobs}%" ] install: [make "install"] diff --git a/meta.yml b/meta.yml index c1ebe00..05fecee 100644 --- a/meta.yml +++ b/meta.yml @@ -9,9 +9,11 @@ synopsis: >- Micromega tactics for Mathematical Components description: |- - This small library enables the use of the Micromega tactics for goals stated - with the definitions of the Mathematical Components library by extending the - zify tactic. + This small library enables the use of the Micromega arithmetic solvers of Coq + for goals stated with the definitions of the Mathematical Components library + by extending the zify tactic. Other than that, the `ssrZ` library provides + some basic MathComp style definitions to reason about the standard integer + type `Z`. authors: - name: Kazuhiko Sakaguchi