The presentation addresses this in a way. The argument is that in Coq you can write proof _scripts_ ("repeat this simplification operation until it does nothing", "pattern match on this definition and apply this operation to every subcase", "proof tactics" and so on), and in this way the same proof script can prove different theorems.

So there is a possibility that changing the code only forces you to change theorem statements (that is, the spec), allowing reuse of the proof script itself. Now you are doing software engineering on proof scripts, and you face the same generality/flexibility problems you would face when writing unit tests. A well-written proof script would be flexible enough, and a hacky one would lock things down too much.