- [Tactics.auto ~dbd ~params ~universe ;
- Tactics.auto ~dbd ~params:params' ~universe]
- | `Term just -> Tactics.apply just
+ [Tactics.auto ~dbd ~params:(univ, params) ~universe ;
+ Tactics.auto ~dbd ~params:(univ, params') ~universe]
+ | `Term just -> Tactics.apply just
+ | `SolveWith term ->
+ Tactics.solve_rewrite ~universe ~params:([term],["steps","1"]) ()
+ | `Proof ->
+ Tacticals.id_tac