https://github.com/MevenBertrand/metacoq
Revision b960d7db28579930105304d22a3c69dc6b5cb8e5 authored by Matthieu Sozeau on 03 March 2020, 15:30:31 UTC, committed by Matthieu Sozeau on 10 March 2020, 13:36:59 UTC
1 parent f698673
Tip revision: b960d7db28579930105304d22a3c69dc6b5cb8e5 authored by Matthieu Sozeau on 03 March 2020, 15:30:31 UTC
Fixed univ.v issue
Fixed univ.v issue
Tip revision: b960d7d
coq-metacoq-checker.opam
opam-version: "2.0"
maintainer: "matthieu.sozeau@inria.fr"
homepage: "https://metacoq.github.io/metacoq"
dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.10"
bug-reports: "https://github.com/MetaCoq/metacoq/issues"
authors: ["Abhishek Anand <aa755@cs.cornell.edu>"
"Simon Boulier <simon.boulier@inria.fr>"
"Cyril Cohen <cyril.cohen@inria.fr>"
"Yannick Forster <forster@ps.uni-saarland.de>"
"Fabian Kunze <fkunze@fakusb.de>"
"Gregory Malecha <gmalecha@gmail.com>"
"Matthieu Sozeau <matthieu.sozeau@inria.fr>"
"Nicolas Tabareau <nicolas.tabareau@inria.fr>"
"Théo Winterhalter <theo.winterhalter@inria.fr>"
]
license: "MIT"
build: [
["sh" "./configure.sh"]
[make "-j%{jobs}%" "checker"]
]
install: [
[make "-C" "checker" "install"]
]
depends: [
"ocaml" {> "4.02.3"}
"coq" {>= "8.10" & < "8.11~"}
"coq-equations" { >= "1.2" }
"coq-metacoq-template" {= version}
]
synopsis: "Specification of Coq's type theory and reference checker implementation"
description: """
MetaCoq is a meta-programming framework for Coq.
The Checker module provides a complete specification of Coq's typing and conversion
relation along with a reference type-checker that is extracted to a pluging.
This provides a command: `MetaCoq Check [global_reference]` that can be used
to typecheck a Coq definition using the verified type-checker.
"""
# url {
# src: "https://github.com/MetaCoq/metacoq/archive/v2.1-beta3.tar.gz"
# checksum: "md5=e81b8ecabef788a10337a39b095d54f3"
# }
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...