Wish : A command for checking correctness of mappings

[agontard]

I would personally gain a lot of time if there was a command available to check the correctness of mappings that could be available even before "make v", for example by obtaining a rocq file from the (name)_terms.lp file that transforms definitions into a "Check" command to check correct names and types for all mapped objects.

[fblanqui]

Isn't make opam what you are looking for?

[agontard]

Isn't make opam what you are looking for?

It does some of it but to me the most important (whose actual types are more likely to change or require to be changed) are the ..._def lemmas, which additionnaly are going to create errors only very late in the proof checking, and they don't appear in (name)_opam.v.