Update doc

math-comp · Sep 29, 2021 · 0baa47a · 0baa47a
1 parent 9f46d94
commit 0baa47a
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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