Merge pull request #3270 from Matafou/libhyps-3.0.1

coq-libhyps 3.01 for 8.20 and all versions.

released/packages/coq-libhyps/coq-libhyps.3.0.1/opam

@@ -0,0 +1,51 @@
+opam-version: "2.0"
+maintainer: "Pierre.Courtieu@lecnam.net"
+synopsis: "Hypotheses manipulation library"
+
+homepage: "https://github.com/Matafou/LibHyps"
+dev-repo: "git+https://github.com/Matafou/LibHyps.git"
+bug-reports: "https://github.com/Matafou/LibHyps/issues"
+doc: "https://github.com/Matafou/LibHyps/blob/master/Demo/demo.v"
+license: "MIT"
+
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+
+install: [make "install"]
+
+depends: [
+  "coq" {(>= "8.11" & < "8.21~") | (= "dev")}
+]
+
+tags: [
+  "keyword:proof environment manipulation"
+  "keyword:forward reasoning"
+  "keyword:hypothesis naming"
+  "category:Miscellaneous/Coq Extensions"
+  "logpath:LibHyps"
+  "date:2024-12-19"
+]
+
+authors: [
+ "Pierre Courtieu"
+]
+
+description: "
+This library defines a set of tactics to manipulate hypothesis
+individually or by group. In particular it allows applying a tactic on
+each hypothesis of a goal, or only on *new* hypothesis after some
+tactic. Examples of manipulations: automatic renaming, subst, revert,
+or any tactic expecting a hypothesis name as argument.
+
+It DOES NOT provide ANYMORE the especialize tactic to ease forward
+reasoning by instantianting one, several or all premisses of a
+hypothesis. Ths is due to coq's specialize being less permissive about
+evars. This may be fixed in the future.
+"
+
+url {
+  src: "https://github.com/Matafou/LibHyps/archive/refs/tags/3.0.1.tar.gz"
+  checksum: "sha512=d29114cd6ed5a4c88283b7598a0720b693bf978c4e5c42d5451e1bf21e8bfdc7d9b0a274ef34b27f8ab97635240628a1349c175bd52fc3acedb993dd3e816548"
+}