fix

affeldt-aist · Nov 20, 2023 · 59dee28 · 59dee28
1 parent b8a5ef8
commit 59dee28
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -40,6 +40,7 @@ information theory, and linear error-correcting codes.
   - [MathComp field](https://math-comp.github.io)
   - [MathComp analysis](https://github.com/math-comp/analysis)
   - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
+  - MathComp algebra tactics
 - Coq namespace: `infotheo`
 - Related publication(s):
   - [Formal Adventures in Convex and Conical Spaces](https://arxiv.org/abs/2004.12713) doi:[10.1007/978-3-030-53518-6_2](https://doi.org/10.1007/978-3-030-53518-6_2)

diff --git a/coq-infotheo.opam b/coq-infotheo.opam
@@ -29,6 +29,7 @@ depends: [
   "coq-mathcomp-field" { (>= "1.16.0" & < "1.19~") | (= "dev")  }
   "coq-mathcomp-analysis" { (>= "0.5.4") & (< "0.7~")}
   "coq-hierarchy-builder" { = "1.5.0" }
+  "coq-mathcomp-algebra-tactics" { = "1.1.1" }
 ]
 
 tags: [

diff --git a/meta.yml b/meta.yml
@@ -90,6 +90,12 @@ dependencies:
     version: '{ = "1.5.0" }'
   description: |-
     [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder)
+- opam:
+    name: coq-mathcomp-algebra-tactics
+    version: '{ = "1.1.1" }'
+  description: |-
+    MathComp algebra tactics
+
 namespace: infotheo
 
 keywords: