-
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
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