diff --git a/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam b/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam index e7bcd24e8c..ab68bea3e1 100644 --- a/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam +++ b/extra-dev/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.dev/opam @@ -12,7 +12,7 @@ This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for the Mathematical Components library. These tactics use the algebraic structures defined in the MathComp library and their canonical instances for the instance resolution, and do not require any special instance declaration, -like the `add Ring` and `Add Field` commands. Therefore, each of these tactics +like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics works with any instance of the respective structure, including concrete instances declared through Hierarchy Builder, abstract instances, and mixed concrete and abstract instances, e.g., `int * R` where `R` is an abstract diff --git a/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam index 18dff2820f..54dcb2063d 100644 --- a/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam +++ b/released/packages/coq-mathcomp-algebra-tactics/coq-mathcomp-algebra-tactics.1.2.2/opam @@ -12,7 +12,7 @@ This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for the Mathematical Components library. These tactics use the algebraic structures defined in the MathComp library and their canonical instances for the instance resolution, and do not require any special instance declaration, -like the `add Ring` and `Add Field` commands. Therefore, each of these tactics +like the `Add Ring` and `Add Field` commands. Therefore, each of these tactics works with any instance of the respective structure, including concrete instances declared through Hierarchy Builder, abstract instances, and mixed concrete and abstract instances, e.g., `int * R` where `R` is an abstract