import ssreflect only once
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
parent
0844b5aa
No related branches found
No related tags found