package rocq-autosubst-ocaml

Autosubst can be used to generate substitution boilerplate code for syntax with binders. It takes language definitions written in signature files and outputs a file that contains Rocq code implementing the language, the substitution operation, rewriting lemmas and a tactic to automatically solve certain substitution goals using the rewriting lemmas.