Error when compiling with Rocq v9.0.0

[mcoulont]

Hello

It was suggested to write to you in Stack Exchange.

I'm in v9.0.0 of Rocq and get this error when I run make:

File "./coq/lib_utils/LibUtilsCoqLibAdd.v", line 33, characters 15-22:
Error: Cannot find a physical path bound to logical path Zdigits.

Your last commit is a bit old, maybe that's why.

[shinnar]

Thanks for your interest in our library. As you noticed, the FormalML library is not yet ported to Rocq 9.XX.

There is work underway to move to Rocq 9.1.0.

[mcoulont]

OK

[shinnar]

@mcoulont good news!

This has been resolved by #22

It is currently verified to build with Rocq 9.0.1.

Please advise if you have any troubles.