Commit 28df8b2c authored by Ralf Jung's avatar Ralf Jung
Browse files

sync autosubst package with coq extra-dev

parent e28300fe
opam-version: "2.0"
name: "coq-autosubst"
maintainer: "Ralf Jung <>"
authors: "Steven Schäfer, Tobias Tebbi"
homepage: ""
maintainer: ""
homepage: ""
dev-repo: "git+"
bug-reports: ""
license: "MIT"
dev-repo: "git+"
synopsis: "Coq library for parallel de Bruijn substitutions"
description: """
Autosubst is a library for the Coq proof assistant which
provides automation for formalizing syntactic theories with
variable binders. Given an inductive definition of syntactic
objects in de Bruijn representation augmented with binding
annotations, Autosubst synthesizes the parallel substitution
operation and automatically proves the basic lemmas about
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/Autosubst"]
depends: [
"coq" {(>= "8.9" & < "8.14~") | (= "dev")}
"coq" {(>= "8.11" & < "8.15~") | (= "dev")}
synopsis: "Autosubst is a Coq library for parallel de Bruijn substitutions"
flags: light-uninstall
tags: [
"category:Computer Science/Lambda Calculi"
"keyword:abstract syntax"
"keyword:de Bruijn indices"
authors: [
"Steven Schäfer"
"Tobias Tebbi"
url {
src: "git+"
src: "git+"
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment