This is to prevent quantified records from being decomposed by
  eval_match. e.g, assert { forall x:t. ... } was previously
  transformed to assert { forall x1:t1, x2:t2, x3:t3. ... } if x was
  a record type with fields x1,x2,x3. This changed the
  instantiation pattern, which could be harmful.