From 62f03a72abdc287c7abdc991c6b7dc73aab1e78e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Mon, 20 Jan 2025 16:09:15 +0100 Subject: [PATCH] add coq-hol-light-real-with-N.1.0.0 --- .../coq-hol-light-real-with-N.1.0.0/opam | 30 +++++++++++++++++++ .../coq-hol-light-real-with-nat.1.0.0/opam | 2 +- 2 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam diff --git a/released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam b/released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam new file mode 100644 index 000000000..ad6c4c404 --- /dev/null +++ b/released/packages/coq-hol-light-real-with-N/coq-hol-light-real-with-N.1.0.0/opam @@ -0,0 +1,30 @@ +opam-version: "2.0" +synopsis: "Definition of HOL-Light real numbers in Coq using N" +description: """ +This library provides a representation in Coq of the definition of real numbers +in HOL-Light, using the Coq type N for natural numbers, automatically generated +from HOL-Light using hol2dk and lambdapi. +""" +homepage: "https://github.com/Deducteam/coq-hol-light-real-with-N" +dev-repo: "git+https://github.com/Deducteam/coq-hol-light-real-with-N.git" +bug-reports: "https://github.com/Deducteam/coq-hol-light-real-with-N/issues" +doc: "https://github.com/Deducteam/coq-hol-light-real-with-N" +maintainer: "frederic.blanqui@inria.fr" +authors: ["Frédéric Blanqui"] +license: "CeCILL-2.1" +depends: [ + "coq" {>= "8.19"} +] +build: [make "-j%{jobs}%"] +install: [make "install"] +tags: [ + "keyword:HOL-Light" + "category:Math/Arith/Misc" + "category:Math/Arith/Real numbers" + "date:2025-01-20" + "logpath:HOLLight_Real" +] +url { + src: "https://github.com/Deducteam/coq-hol-light-real-with-N/archive/refs/tags/1.0.0.tar.gz" + checksum: "sha256=97895ee619541adf57617f23ea975489f5ceac7be718b03e7f45ac7d878cb479" +} diff --git a/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam b/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam index 59571f472..074ef0eff 100644 --- a/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam +++ b/released/packages/coq-hol-light-real-with-nat/coq-hol-light-real-with-nat.1.0.0/opam @@ -1,5 +1,5 @@ opam-version: "2.0" -synopsis: "Definition of HOL-Light real numbers in Coq" +synopsis: "Definition of HOL-Light real numbers in Coq using nat" description: """ This library provides a representation in Coq of the definition of real numbers in HOL-Light using the Coq type nat for natural numbers, automatically generated