(string option * Cic.term) option -> Cic.term ->
[ `Term of Cic.term | `Auto of (string * string) list ] ->
bool (* last step *) -> ProofEngineTypes.tactic
(string option * Cic.term) option -> Cic.term ->
[ `Term of Cic.term | `Auto of (string * string) list ] ->
bool (* last step *) -> ProofEngineTypes.tactic