Problems with bil.ott

[bowtochris]

When I use the command "ott -i bil.ott -o bil.v", I get the message "meta or sugar production must have a hom for each target - here "coq" is missing" I'm probably missing something obvious.

[ivg]

The master branch is indeed missing Coq homs, try the coq-formalization branch that has them.