coq-hol-light-real.opam

opam-version: "2.0"
synopsis: "HOL-Light definition of real numbers in Coq"
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: [
  "keyword:HOL-Light"
  "category:Math/Arith/Misc"
  "category:Math/Arith/Real numbers"
  "date:2024-11-03"
  "logpath:HOLLight_Real"
]