[classes] Some refactoring on proof save preparation.

Note the ugly problem that we have on close_proof:
```
proof_global.ml:278

  let entry_fn p (_, t) =
    let t = EConstr.Unsafe.to_constr t in
    let univstyp, body = make_body t p in
```
arguments of start_proof should be pre-normalized.

I think this will require a lot of refactoring to be fixed properly.

0 files changed, 0 insertions, 0 deletions