• Martin Clochard's avatar
    Hack to prevent eval-match from decomposing quantified records · 698ca990
    Martin Clochard authored
      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.
    698ca990
eval_match.ml 6.75 KB