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

0 files changed, 0 insertions, 0 deletions