Skip to content

Import ssreflect only once

Sergey Bozhko requested to merge sbozhko/rt-proofs:fix-prosa-done into master

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.

Merge request reports