Change specification of declared constant and co

[tabareau]

This PR changes the definition of declared_constant and declared_minductive
to make us of In instead of the more operational lookup_env approach.

[tabareau]

I am not sure that the way I have adapted some proofs is optimal, in particular in Erasure, but those proofs are not very well structured, so it seems hard to organize better without a huge refactoring.

[yannl35133]

I may be missing some context, but what is the issue with the existing definitions ? Are the _gen variants still useful ?

[tabareau]

The idea is that the use of lookup_global in the specification was a bit to concrete, using In seems more accurate. The _gen variants are used to relate the abstract specification to presentation using a concrete or abstract lookup function. In PCUIC, we use the concrete lookup because it provides simple reasoning. In Safechecker we use an abstract lookup that is latter instantiated with an efficient lookup on AVL trees.

[tabareau]

I may be missing some context, but what is the issue with the existing definitions ? Are the _gen variants still useful ?

@yannl35133 sorry, I wanted to assign the PR to Yannick but I misclicked.

[yannl35133]

Right, that makes more sense

[yforster]

The amount of unshelve epose proof (...); eauto lets me think that there should be a primitive in Coq for something like that

[JasonGross]

Does this conflict with #816?

[tabareau]

I don't think it conflicts with #816 as it mainly changes basic definitions in EnvironmentTyping.v, which is almost not touched by #816. It should not be difficult to merge one after the other. We will see that beginning of January.