STM/Univ: save initial univs (the ones in the statement) in Proof.proof

This makes the treatment of universe constraints/normalization more
understandable in the Sync/Async case:
- if one has to keep the constraints of the body and the type of
  a lemma separate, then equations coming from the body are kept
  (see: 866c41 )
- if they can be merge then the equations (substituted on both the
  body and type) can be removed (one of the sides occurs nowhere)

The result is that, semantically, the constraints of a lemma do not
depend on weather it was produced asynchronously (v->vio->vo, or in
a CoqIDE session) or synchronously (v->vo).

Still the internal representation of the constraints changes to
accommodate an optimization (to reduce the size of the constraint set):
- in the synchronous case (some) equations are substituted (in both the
  type and body), hence they can be completely dropped from the constraint
  set
- in the asynchronous case (some) equations are substituted in the body
  only (the type is fixed once and for all before the equations are
  discovered/generated), hence these equations are necessary to relate
  the type and the (optimized) body and are hence kept in the constraint
  set

1 files changed, 1 insertions, 0 deletions

diff --git a/proofs/proof.mli b/proofs/proof.mli
index 2b85ec872..a2e10d813 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -69,6 +69,7 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
 val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_euctx : proof -> Evd.evar_universe_context
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)