Changes to the Ackermann sub-library

[Casteran]

In the files inherited from Goedel (now in theories/Ackermann), the predicates isPR and isPRrel are of sort Set, but all the proofs of primitive recursivity were opaque (endind by Qed), which forbids us from analysing the implementation of a proven primitive recursive function (code size, for instance).

It happens that changing all Qed into Defined is the proofs of primitive recursivity breaks the compilation of the goedel library (a repeated ltac tactic at line 1552 of codeSysPrf.v loops).

The branch transparent-IsPR restricts this change opaque->transparent to a few modules of Ackermann, so as to prevent the compilation of goedel to fail. If it's OK, I propose to merge it into master.

[Zimmi48]

Sounds reasonable. Another solution would be to adapt Goedel to work with these changes.

[Casteran]

Yes, I will try to understand which lemma should remain or made opaque (or simply not being unfolded) in Goedel.
Meanwhile, I will maintain two branches in hydra-battles.