Extracted code is checked into version control

[palmskog]

The staltac tactic is produced from code in version control that was previously extracted, then manually copied into an OCaml file, and mixed with imperative code. The proper way to do this is to have a project build extract the relevant code every time, and link it with the imperative code to produce the tactic.