Call Evd.nf_constraints only on Univ Poly constants

When one generates a .vi file only the type is stocked.
When one completes a .vi the proof term is stocked but the
corresponding type is not changed:
- if one minimizes the constraints of the body, the minimization
  could find that 2 univs are equal and substitute one for the
  other in the body, but it should also apply the subst to the type
  orelse coqchk could fail
- also, a "retroactive" change of a type (making it stricter)
  invalidates what was type checked afterwards, so this operation
  clashes with the vi2vo compilation chain
Hence we enable this optimization only for universe polymorphic
constants that:
- are the ones that truly requires such optimization
- are never processed asynchronously, so the scenario above does
  not apply

1 files changed, 2 insertions, 2 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 79e86e7a9..d94bc86cd 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -338,7 +338,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
 
 let return_proof () =
-  let { proof } = cur_pstate () in
+  let { proof; strength = (_,poly,_) } = cur_pstate () in
   let initial_goals = Proof.initial_goals proof in
   let evd =
     let error s = raise (Errors.UserError("last tactic before Qed",s)) in
@@ -353,7 +353,7 @@ let return_proof () =
         error(str"Attempt to save a proof with existential " ++
               str"variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd = Evd.nf_constraints evd in
+  let evd = if poly then Evd.nf_constraints evd else 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... *)