(string option * Cic.term) option -> Cic.term ->
[ `Term of Cic.term | `Auto of Auto.auto_params
| `Proof | `SolveWith of Cic.term] ->
(string option * Cic.term) option -> Cic.term ->
[ `Term of Cic.term | `Auto of Auto.auto_params
| `Proof | `SolveWith of Cic.term] ->