rename tactic enabled,
rewrite and rewrite_simpl now take optional names for the rewrited premises
- procedural script reconstruction
now starts directly from acic bypassing the content level,
the script for the use case proof in matita/contribs/prova.ma is reconstructed completely now and is correctly parsed and typechecked