From 37897600e120faeeadd39131380bd2f2497fbbba Mon Sep 17 00:00:00 2001
From: Aleksandar Nanevski <aleks.nanevski@imdea.org>
Date: Mon, 30 Sep 2024 16:18:48 +0200
Subject: [PATCH] templates

---
 .github/workflows/docker-action.yml        | 1 +
 README.md                                  | 1 +
 coq-htt-core.opam                          | 1 +
 coq-htt.opam                               | 2 ++
 meta.yml                                   | 4 ++++
 templates-extra/coq-htt.opam.mustache      | 2 +-
 templates-extra/docker-action.yml.mustache | 2 +-
 7 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 761fe01..94ff297 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -1,4 +1,5 @@
 # This file was generated from `meta.yml`, please do not edit manually.
+
 name: Docker CI
 
 on:
diff --git a/README.md b/README.md
index e9a1336..8213b20 100644
--- a/README.md
+++ b/README.md
@@ -43,6 +43,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
 - Additional dependencies:
   - [MathComp ssreflect 2.2](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
+  - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm)
   - [Dune](https://dune.build) 2.5 or later
 - Coq namespace: `htt`
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index 95ee94a..1a20705 100644
--- a/coq-htt-core.opam
+++ b/coq-htt-core.opam
@@ -37,6 +37,7 @@ depends: [
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-mathcomp-algebra" 
+  "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }
 ]
 
diff --git a/coq-htt.opam b/coq-htt.opam
index 7086e27..88df21e 100644
--- a/coq-htt.opam
+++ b/coq-htt.opam
@@ -1,4 +1,5 @@
 # This file was generated from `meta.yml`, please do not edit manually.
+
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
 version: "dev"
@@ -35,6 +36,7 @@ depends: [
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
   "coq-mathcomp-algebra" 
+  "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }
 ]
 
diff --git a/meta.yml b/meta.yml
index 9459fe1..b8388ff 100644
--- a/meta.yml
+++ b/meta.yml
@@ -101,6 +101,10 @@ dependencies:
     name: coq-mathcomp-algebra
   description: |-
     [MathComp algebra](https://math-comp.github.io)
+- opam: 
+    name: coq-mathcomp-fingroup
+  description: |-
+    [MathComp fingroup](https://math-comp.github.io)
 - opam:
     name: coq-fcsl-pcm
     version: '{ (>= "2.0.0" & < "2.1~") | (= "dev") }'
diff --git a/templates-extra/coq-htt.opam.mustache b/templates-extra/coq-htt.opam.mustache
index 91e12ca..2d53c31 100644
--- a/templates-extra/coq-htt.opam.mustache
+++ b/templates-extra/coq-htt.opam.mustache
@@ -1,4 +1,4 @@
-; This file was generated from `meta.yml`, please do not edit manually.
+# This file was generated from `meta.yml`, please do not edit manually.
 
 opam-version: "2.0"
 maintainer: "{{& opam-file-maintainer }}{{^ opam-file-maintainer }}palmskog@gmail.com{{/ opam-file-maintainer }}"
diff --git a/templates-extra/docker-action.yml.mustache b/templates-extra/docker-action.yml.mustache
index 89cf25b..9866673 100644
--- a/templates-extra/docker-action.yml.mustache
+++ b/templates-extra/docker-action.yml.mustache
@@ -1,4 +1,4 @@
-; This file was generated from `meta.yml`, please do not edit manually.
+# This file was generated from `meta.yml`, please do not edit manually.
 
 name: Docker CI