Compilation error with successive binders #8
Description
The .v file generated by autosubst on a signature file with multiple binders in a single item seems to go wrong when used with the option -allfv.
Example signature file (bug.sig):
term : Type
F : (bind term, term in term) -> term
Autosubst called with:
$ autosubst -s ucoq -v ge813 -allfv bug.sig -o Ast.v
The problem lie in the functions allfvRenL_term and allfvRenR_term in the generated Ast.v. The bug seems easy to fix (add additional helper functions similar to the ones already generated, see full repro attached).
repro.zip