Skip to content
  • Sergey Bozhko's avatar
    import ssreflect only once · e8f5fb9a
    Sergey Bozhko authored and Björn Brandenburg's avatar Björn Brandenburg committed
    Prosa redefines ssreflect's tactic [done] in file [util/tactics.v]. To prevent shadowing of the new [done] by ssreflect's [done], [tactics.v] should be imported _after_ ssreflect
    e8f5fb9a