Skip to content

Use mathcomp's int instead of stdlib's Z

Pierre Roux requested to merge proux1/rt-proofs:use_int into master

int is convenient for proofs whereas Z is more oriented towards more efficient computations. Since we are using nat (proof oriented) along our integers, there is no point in using Z.

@kbedarka I'll offer you a rebase of your elf_rta branch once this is merged

Merge request reports