Synchronize set_strategy with the discharge/load infrastructure

[herbelin]

To register the opacity of lemmas generated by equations, the current code, except for issue #83, directly calls Safe_typing.set_strategy. This PR synchronizes the occurrences of Safe_typing.set_strategy corresponding to the registration of a constant with the discharge/load mechanism, and, suspectingly, this would solve other issues similar to #83 for other kinds of registered lemmas.

Additionally, the PR would be necessary to eventually go in the direction of PR coq/coq#17888 (discharge on the fly).

If I'm correct, that's the occurrences in noconf_hom.ml, equations.ml, and principles.ml, but not the ones in principles_proofs.ml

As for the first Safe_typing.set_strategy in principles.ml used in the inOpacity object, I believe that the EQUATIONS_OPACITY object can directly be replaced by Coq's STRATEGY object which already plays the same purpose.

[herbelin]

As far as I can judge, this PR seems to really fix a bug: the opaque status of _unfold definitions is currently not preserved at End SomeSection time nor at Require time. This is actually even exploited in the line unfold reduce_stack_full_unfold of PCUICRetypingEnvIrrelevance.v in metacoq.