val rewritingstep :
dbd:HSql.dbd -> universe:Universe.universe ->
(string option * Cic.term) option -> Cic.term ->
- [ `Term of Cic.term | `Auto of (string * string) list ] ->
+ [ `Term of Cic.term | `Auto of (string * string) list | `Proof ] ->
bool (* last step *) -> ProofEngineTypes.tactic