coq-hol-light-real-with-N.opam

opam-version: "2.0"
synopsis: "HOL-Light definition of real numbers in Coq using N"
description: """
This library contains an automatic translation in Coq of the HOL-Light
definition of real numbers using https://github.com/Deducteam/hol2dk.
"""
homepage: "https://github.com/Deducteam/coq-hol-light-real"
dev-repo: "git+https://github.com/Deducteam/coq-hol-light-real.git"
bug-reports: "https://github.com/Deducteam/coq-hol-light-real/issues"
doc: "https://github.com/Deducteam/coq-hol-light-real"
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: [
  "logpath:HOLLight_Real_With_N"
  "date:2025-01-21"
  "category:Math/Arith/Misc"
  "category:Math/Arith/Real numbers"
  "keyword:HOL-Light"
]