Compilation error

[francesco-bongiovanni]

Hi (again),

I downloaded the last version of codegen but unfortunately I have the following error when I try to compile it:

COQC theories/verify.v
File "./theories/verify.v", line 302, characters 13-57:
Error: Unbound value Constr.Pretype.Flags.open_constr_flags_no_tc

make[2]: *** [Makefile.coq:848: theories/verify.vo] Error 1
make[2]: *** [theories/verify.vo] Deleting file 'theories/verify.glob'
make[1]: *** [Makefile.coq:417: all] Error 2
make[1]: Leaving directory '/home/fbongiov/SaveUbuntu20.04/home/coq_projects/codegen'
make: *** [Makefile:6: all] Error 2

I have installed Coq v 8.19.0 under the OCaml 5.1.1 as suggested.

Do you have any idea what is wrong ?

Kind regards.

Francesco

[akr]

Oops. I forgot to update README.md.
codegen needs Coq 8.20 now.
Thank you.

[francesco-bongiovanni]

Thanks a lot ! I confirm that it works now.

Kind regards.

Francesco