Hi,
I was having issues running this in Coq 8.19.
The following minor changes fixed the issues for me:
- Replacing
plus_0_r and plus_0_l with Nat.add_0_r and Nat.add_0_l in DeBruijn.v .
- Replacing
elimtype False with exfalso in Environments.v
I have made a corresponding pull request: #15