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

3 files changed, 25 insertions, 20 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 828f9fa71..a7077d911 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -111,6 +111,8 @@ type proof = {
   shelf : Goal.goal list;
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
+  (* The initial universe context (for the statement) *)
+  initial_euctx : Evd.evar_universe_context
 }
 
 (*** General proof functions ***)
@@ -271,7 +273,9 @@ let start sigma goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 let dependent_start goals =
   let entry, proofview = Proofview.dependent_init goals in
@@ -280,7 +284,9 @@ let dependent_start goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
@@ -311,6 +317,7 @@ let return p =
     Proofview.return p.proofview
 
 let initial_goals p = Proofview.initial_goals p.entry
+let initial_euctx p = p.initial_euctx
 
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
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). *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8be96285f..3e2c813e3 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -273,12 +273,10 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
+  let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
-  let universes = 
-    if poly || now then Future.force univs 
-    else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) 
-  in
-  (* Because of dependent subgoals at the begining of proofs, we could
+  let universes = if poly || now then Future.force univs else initial_euctx in
+  (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
   let subst_evar k =
@@ -289,11 +287,12 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
     if poly || now then
       let make_body t (c, eff) =
         let open Universes in
-	let body = c and typ = nf t in
+        let body = c and typ = nf t in
         let used_univs_body = Universes.universes_of_constr body in
-	let used_univs_typ = Universes.universes_of_constr typ in
-	let ctx = Evd.evar_universe_context_set Univ.UContext.empty universes in
+        let used_univs_typ = Universes.universes_of_constr typ in
         if keep_body_ucst_sepatate then
+          let initunivs = Evd.evar_context_universe_context initial_euctx in
+          let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
@@ -302,6 +301,8 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
           let univs_typ = Univ.ContextSet.to_context ctx_typ in
           (univs_typ, typ), ((body, ctx_body), eff)
         else
+          let initunivs = Univ.UContext.empty in
+          let ctx = Evd.evar_universe_context_set initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
            * constraints in which we merge the ones for the body and the ones
            * for the typ *)
@@ -310,14 +311,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
           let univs = Univ.ContextSet.to_context ctx in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
-	fun t p ->
-	  Future.split2 (Future.chain ~pure:true p (make_body t))
+       fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
     else
       fun t p ->
-        let initunivs = Evd.evar_context_universe_context universes in
-	  Future.from_val (initunivs, nf t), 
-	  Future.chain ~pure:true p (fun (pt,eff) ->
-	    (pt, Evd.evar_universe_context_set initunivs (Future.force univs)), eff)
+        let initunivs = Evd.evar_context_universe_context initial_euctx in
+        Future.from_val (initunivs, nf t),
+        Future.chain ~pure:true p (fun (pt,eff) ->
+          (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff)
   in
   let entries =
     Future.map2 (fun p (_, t) ->
@@ -370,10 +370,7 @@ let return_proof ?(allow_partial=false) () =
     | Proof.HasUnresolvedEvar->
         error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd =
-    if poly || !Flags.compilation_mode = Flags.BuildVo
-    then Evd.nf_constraints evd
-    else evd in
+  let evd = Evd.nf_constraints evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)