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