Skip to content

Add autosubst-ocaml to the Coq Platform #455

Open
@palmskog

Description

@palmskog

autosubst-ocaml is an OCaml reimplementation of the (seemingly unmaintained) Autosubst 2 code generator. Autosubst 2 in turn is based on previous work on Autosubst, but is a code generator rather than a Coq library.

To improve the Platform's support for programming language metatheory, I propose that autosubst-ocaml is included. Technically, autosubst-ocaml interfaces with Coq's API and is part of Coq's CI.

@yforster, can you confirm here that releases/tags can be done of autosubst-ocaml for every major Coq/Rocq version? The work should be minimal for this since updates will come via Coq's CI.

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions