Make [Proof_global.closed_proof_output] opaque

This means return_proof is the only place where it can be produced.

We need to change the stm a bit as it keeps a pointer to a
[closed_proof_output] to join and to check if it failed, and it needs
a way to create a dummy in 1 case.

I'm not sure if this works correctly though, how to test?

We also inline the used bits of [return_proof ~allow_partial:true] in
[save_lemma_admitted] to get [Proof using] info. We could
alternatively expose the [closed_proof_output -> constr list]
projection. I think the code is easier to understand this way though,
as we don't have to read [return_proof] and figure out that the side
effect manipulation is ignored etc.

Note that the "this will warn" comment was outdated since
73daf37ccc7a44cd29c9b67405111756c75cb26a

0 files changed, 0 insertions, 0 deletions