Merge pull request #3214 from DmxLarchey/KruskalThms-1.2

Update coq-kruskal-[veldman,theorems] to account for Coq 8.20 and SWHID

released/packages/coq-kruskal-theorems/coq-kruskal-theorems.1.2/opam

@@ -0,0 +1,41 @@
+opam-version: "2.0"
+synopsis: "Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem"
+description: """
+   This library formalizes the high-level variants of Higman's theorem (for trees of bounded arity)
+   and Kruskal's theorem (for rose trees), depending on how these datatypes are implemented. Also,
+   Vazsonyi's conjecture to illustrate the expressive power of Kruskal's and Higman's theorem.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-Theorems/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-Theorems/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Theorems/"
+
+build: [
+  [make "-j%{jobs}%" "type"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq-kruskal-trees"
+  "coq-kruskal-almostfull"
+  "coq-kruskal-higman" {>= "1.3"}
+  "coq-kruskal-veldman" {>= "1.3"}
+]
+
+url {
+  src: "https://github.com/DmxLarchey/Kruskal-Theorems/releases/download/1.2/Kruskal-Theorems-1.2.tar.gz"
+  checksum: [
+    "sha256=fcaae51f970d68be837dac59520d0aae0bbaba1d522d9e25466580c3f1c2646d"
+  ]
+}
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "date:2024-08-28"
+  "logpath:KruskalThmProp"
+  "logpath:KruskalThmType"
+]

released/packages/coq-kruskal-veldman/coq-kruskal-veldman.1.3/opam

@@ -0,0 +1,42 @@
+opam-version: "2.0"
+synopsis: "Wim Veldman's proof of Higman's and Kruskal tree theorems"
+description: """
+   This library formalizes additional tools for AF relations, eg AF lexicographic induction 
+   and relational quasi morphisms applied to Wim Veldman's constructive proof of the tree theorem.
+"""  
+maintainer: ["Dominique Larchey-Wendling (https://github.com/DmxLarchey)"] 
+authors: "Dominique Larchey-Wendling (https://github.com/DmxLarchey)"
+license: "MPL-2.0"
+homepage: "https://github.com/DmxLarchey/Kruskal-Veldman/"
+bug-reports: "https://github.com/DmxLarchey/Kruskal-Veldman/issues"
+dev-repo: "git+https://github.com:DmxLarchey/Kruskal-Veldman/"
+
+build: [
+  [make "-j%{jobs}%" "prop"]
+]
+install: [
+  [make "install"]
+]
+
+depends: [
+  "coq-kruskal-trees"
+  "coq-kruskal-finite"
+  "coq-kruskal-almostfull"
+  "coq-kruskal-fan"    {>= "1.2"}
+  "coq-kruskal-higman" {>= "1.3"}
+]
+
+url {
+  src: "https://github.com/DmxLarchey/Kruskal-Veldman/releases/download/1.3/Kruskal-Veldman-1.3.tar.gz"
+  checksum: [
+    "sha256=0a2e33bb394709bd5eb723d5bd47a25770fb8129d0fff5fb83ca44916f3da210"
+  ]
+}
+
+tags: [
+  "category:Computer Science/Data Types and Data Structures"
+  "date:2024-11-24"
+  "logpath:KruskalVeldmanProp"
+  "logpath:KruskalVeldmanType"
+]
+