Preprocessing tactics
Add the possibility to specify a preprocessing tactic, which is applied on each goal before the strategy.
Note that I finally chosen to explicitly include the tactic in the proof certificate (see tests/preprocess.t)
Edited by Benjamin Jorge