Acic2Procedural:

Acic2Procedural:
 now we accept an optional string argument "info" intended as a comment for the  rendered proof (appears afer qed)
ProceduralOptimizer:
 - we generate some comments for acic2Procedural.ml info (see above)
 - optimize_term is now available
ApplyTransformation:
 we fixed a bug in the procedural rendering of auto proofs:
 the proof term must be optimized before rendering!
 (it is written on the paper about the procedural rendering for PLMMS 2007)