[proof] Split delayed and regular proof closing functions, part I

We split the `close_proof` into two variants, one for delayed proof,
and one for the regular proof closing path, _à la_ interactive.

This makes sense as the typing in both cases is different, even if we
still haven't changed it.

We strongly enforce the invariant (for now) that universe polymorphic
proofs cannot be delayed using this API, as the STM expects.

It introduces some minimal, non-interesting code duplication, which
will go away in the next commits.

0 files changed, 0 insertions, 0 deletions