Merge pull request #15 from palmskog/fingroup-dep

add missing fingroup dependency to README and opam
coq-community · Oct 28, 2021 · 629541d · 629541d
2 parents 984e4ee + f7c02ef
commit 629541d
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -28,6 +28,7 @@ sorting with extended guarantees for acyclic graphs.
 - Compatible Coq versions: 8.10 or later
 - Additional dependencies:
   - [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
+  - [MathComp fingroup](https://math-comp.github.io)
 - Coq namespace: `mathcomp.tarjan`
 - Related publication(s):
   - [Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle](https://hal.inria.fr/hal-01906155) doi:[10.4230/LIPIcs.ITP.2019.13](https://doi.org/10.4230/LIPIcs.ITP.2019.13)

diff --git a/coq-mathcomp-tarjan.opam b/coq-mathcomp-tarjan.opam
@@ -22,6 +22,7 @@ install: [make "install"]
 depends: [
   "coq" {(>= "8.10" & < "8.15~") | (= "dev")}
   "coq-mathcomp-ssreflect" {(>= "1.12.0" & < "1.14~") | (= "dev")}
+  "coq-mathcomp-fingroup" 
 ]
 
 tags: [

diff --git a/meta.yml b/meta.yml
@@ -56,6 +56,10 @@ dependencies:
     version: '{(>= "1.12.0" & < "1.14~") | (= "dev")}'
   description: |-
     [MathComp ssreflect 1.12 or later](https://math-comp.github.io)
+- opam:
+    name: coq-mathcomp-fingroup
+  description: |-
+    [MathComp fingroup](https://math-comp.github.io)
 
 tested_coq_opam_versions:
 - version: 'coq-dev'